第03講：形式化方法及SA的形式化描述

1、哈爾濱工業(yè)大學(xué)計算機(jī)學(xué)院唐好選Email:PART1：基本概念基本概念u形式化方法（Formal Method）的基本含義是借助數(shù)學(xué)的方法來研究計算機(jī)科學(xué)中的有關(guān)問題u形式化方法提供了一個框架，在框架中可以用數(shù)學(xué)的方式開發(fā)和驗證系統(tǒng)。換句話說，在軟件開發(fā)的全過程中，凡是采用嚴(yán)格的數(shù)學(xué)語言，具有精確的數(shù)學(xué)語義的方法，都可稱為形式化的方法其中,L： 表示形式規(guī)格描述語言 Cn：表示字符串中的映射,由推理規(guī)則組成形式化方法的表示形式化方法的表示形式化方法=(1) 面向模型的方法：也稱為基于狀態(tài)的形式化方法 利用一些已知特性的數(shù)學(xué)抽象（域、元組、集合、序列、包、映射等）為目標(biāo)軟件的狀態(tài)特征和行為特征構(gòu)

2、造模型，如Z (2) 代數(shù)方法：通過分析不同操作間的行為關(guān)系給出操作的隱式定義，而不定義狀態(tài)，支持描述結(jié)構(gòu)化 代數(shù)方法僅使用一階邏輯（包括命題邏輯和謂詞邏輯）表示，而不引入通常的數(shù)學(xué)對象，如:OBJ,CLEAR等語言形式化方法的分類形式化方法的分類(3)基于進(jìn)程代數(shù)方法：給出并發(fā)進(jìn)程的一個顯式模型,并通過進(jìn)程間的約束來表示行為(4) 基于邏輯的方法：采用邏輯描述系統(tǒng)的特性，包括程序行為的低級規(guī)范和系統(tǒng)行為規(guī)范,如:時態(tài)邏輯(5) 基于網(wǎng)絡(luò)的方法：根據(jù)網(wǎng)絡(luò)中的數(shù)據(jù)流顯式地給出系統(tǒng)的并發(fā)模型,包括數(shù)據(jù)在網(wǎng)中從一個結(jié)點流向另一個結(jié)點的條件.如:Petri網(wǎng)形式化方法的分類形式化方法的分類u上述方法之

3、間的界限并不完全清晰，有些是結(jié)合多種方法的多個方面而形成的混成(hybrid)方法u大多數(shù)方法都以集合論和謂詞邏輯作為基礎(chǔ)。所以,這些方法在技術(shù)上都有相似性。但在表達(dá)能力上有一定區(qū)別，這也是分類的主要依據(jù)u形式化方法可通過兩種不同方式來使用u可用于生成規(guī)范，并將此規(guī)范作為系統(tǒng)開發(fā)基礎(chǔ)u可將其作為驗證系統(tǒng)正確性的依據(jù)形式化方法的分類形式化方法的分類p有限狀態(tài)機(jī)pPetri網(wǎng)pZ方法基于模型的形式化方法基于模型的形式化方法u通過模型表示系統(tǒng)應(yīng)滿足所定義的行為集合的性質(zhì),具體包括：安全性質(zhì) 和 活動性質(zhì)(1)安全性質(zhì) 給出一個性質(zhì)，對系統(tǒng)的所有執(zhí)行應(yīng)保持成立?？捎脮r態(tài)邏輯表示安全性： P 狀態(tài)公式，

4、表示性質(zhì) 時態(tài)算子，表示“必然” 例如：對于命題P：火星上有生命，那么 P表示火星上必然有生命基于模型的方法基于模型的方法實例R是一非共享資源,N個用戶進(jìn)程使用分配器（AR）管理對資源R的存取用戶進(jìn)程Ui使用資源R前，向AR發(fā)出請求，當(dāng)R可自由存取時，AR作反應(yīng)標(biāo)志用戶進(jìn)程Ui使用完R時，向AR發(fā)出信號釋放R在請求資源到獲悉分配到資源間任意時刻，用戶進(jìn)程可取消請求 安全需求系統(tǒng)必須保證在任何時刻R不會分配給多于一個的Ui模型方法的安全性質(zhì)（例）模型方法的安全性質(zhì)（例）u 資源分配器（AR）的規(guī)格說明: 選擇的動作Request (i): Ui請求存?。ˋR的輸入）Cancel (i): Ui取

5、消未完成的請求 （AR的輸入）Grant (i): Ui被授權(quán)獲得存取（AR的輸出）Finish (i): Ui釋放資源（AR的輸入）模型方法的安全性質(zhì)（例）模型方法的安全性質(zhì)（例）u動作類型表示: 動作名WHEN 條件DO表達(dá)式可表示為三元組: ( s, a, s ) 其中 s為狀態(tài),由 決定 a為 s由對狀態(tài)變量賦值決定模型方法的安全性質(zhì)模型方法的安全性質(zhì)Ui請求請求R : Request (i) WHEN True Do reqi:=True取消取消: Cancel (i) WHEN True Do reqi:=False釋放釋放: Finish (i) WHEN True Do gra

6、nti:= False被授權(quán)被授權(quán): Grant (i) WHEN (reqi AND j, Grant j ) Do Grant(i):=True, reqi:= False模型方法的安全性質(zhì)（例）模型方法的安全性質(zhì)（例） 斷言某事最終必然發(fā)生。有了活動，安全性質(zhì)才有意義。用時態(tài)邏輯表示: (P G) , 即P成立,導(dǎo)致G必然會滿足 模型滿足的活動性質(zhì)：若任意用戶提出請求且未取消，則分配器最終必會授權(quán)該用戶使用資源u一個有限狀態(tài)機(jī)可表示為一個五元組(Q,q0,F) 其中: Q: 是一個有限、非空狀態(tài)集; :是一個有限、非空輸入集; :是一個從(Q F)轉(zhuǎn)換到Q的函數(shù),稱為轉(zhuǎn)換函數(shù)或變遷函數(shù);

7、 q0: q0 Q是初始狀態(tài); F: 是最終狀態(tài)集,F Q每個轉(zhuǎn)換有下列格式 當(dāng)前狀態(tài) and 事件 下一個狀態(tài) 擴(kuò)展 FSM 可表示為一個六元組 (Q,q0,F,P) 其中P為一個謂詞(Predicate)集,每個謂詞是產(chǎn)品的全局狀態(tài)Y的函數(shù),轉(zhuǎn)換函數(shù)是從(Q F)P轉(zhuǎn)換為Q的函數(shù)轉(zhuǎn)換規(guī)則: 當(dāng)前狀態(tài) and 事件 and 謂詞 下一個狀態(tài)節(jié)點節(jié)點狀態(tài)狀態(tài)q q弧弧 輸入輸入k k后狀態(tài)的變化，由狀態(tài)后狀態(tài)的變化，由狀態(tài)q qi i指向指向q qj j的的變遷函數(shù)表示為：變遷函數(shù)表示為：jiqkq),FSM 圖的一般表示方式圖的一般表示方式um層樓n部電梯的大樓服務(wù)系統(tǒng):每個電梯有一組m個按

8、鈕,每層用一個。當(dāng)按下并讓電梯到達(dá)相應(yīng)的層時,這些按鈕燈亮，當(dāng)電梯到達(dá)相應(yīng)層時燈滅除了第一層和頂層,每一層都有兩個按鈕(請求電梯向上、向下)，按下時燈亮,電梯到達(dá)時燈滅沒有對電梯請求時,電梯停留在當(dāng)前樓層,門關(guān)閉u考慮電梯正常運行情況，電梯處于兩個樓層之間時不會停止，并且不會改變運動方向電梯按鈕(Elevator Button ,EB)樓層按鈕(Floor Button ,FB) 1) 電梯按鈕狀態(tài)圖如下：電梯按鈕狀態(tài)電梯按鈕狀態(tài)EBOFF (e,f)EBON (e,f)EAF (e,f)電梯電梯e到達(dá)樓層到達(dá)樓層f電梯按鈕關(guān)閉電梯按鈕關(guān)閉電梯按鈕開啟電梯按鈕開啟按下電梯按鈕按下電梯按鈕EBP

9、 (e,f) 定義事件、狀態(tài)和狀態(tài)轉(zhuǎn)換規(guī)則 謂詞 V(e,f) : 電梯e到達(dá)(停在)樓層f 轉(zhuǎn)換規(guī)則: (1) 當(dāng)前狀態(tài)：電梯按鈕關(guān)，按下按鈕(e,f)，電梯e 沒有到達(dá)樓層f。按鈕開啟 EBOFF (e,f) and EBP (e,f) and not V (e,f) EBON (e,f) (2) 若電梯正到達(dá)樓層，什么也不發(fā)生 (3) 如果電梯到達(dá)樓層f，且按鈕處于開啟狀態(tài), 那么關(guān)閉電梯按鈕 EBON (e,f) and V (e,f) EBOFF (e,f) 2) 樓層按鈕樓層按鈕(FB)狀態(tài)圖狀態(tài)圖定義謂詞 S(d,e,f):是一個狀態(tài),表示電梯e到達(dá)樓層f且移動方向或向上(d=U

10、)、向下(d=D)或掛起(d=N)FBOFF (d,f)FBON (d,f)EAF (1n,f)電梯電梯1 或或n 到達(dá)樓層到達(dá)樓層 f樓層按鈕的狀態(tài)按下樓層按下樓層 f 按鈕按鈕,向向d 方向移動方向移動FBP (d,f)使用S(d,e,f),轉(zhuǎn)換規(guī)則為: (1) 樓層按鈕開啟條件: 樓層f的d方向移動按鈕關(guān)閉，按下該按鈕且無向d方向移動的電梯到達(dá)f 層 FBOFF (d,f) and FBP (d, f) and not S(d,1n,f) = FBON(d,f) (2) 樓層按鈕關(guān)閉條件: 若該按鈕開啟,且最少有一個電梯到達(dá)樓層f并向d方向移動FBON (d,f) and EAF (1n

11、,f) and S(d,1n,f) = FBOFF(d,f), d=U或D 謂詞 V(e,f) ，電梯e到達(dá)(停在)樓層f也可以定義為: V(e f) = S(U,e,f) or S(D,e,f)3) 電梯狀態(tài) M(d,e,f) :電梯e正向d方向移動,即將到達(dá)樓層f; S(d,e,f): 電梯e停在樓層f; W(e,f): 電梯e正在樓層f等待(門關(guān)閉); DC(e,f): 在樓層f,電梯e的門關(guān)閉; ST(e,f): 隨著電梯e接近樓層f,觸發(fā)傳感器 RL: 按下按鈕 S(U,e,f) and DC(e,f) = M(U,e,f+1): 電梯e處于狀態(tài)S(U,e,f)，即停在要上到的樓層,

12、且電梯門關(guān),則該電梯將向上移動到下一層; S(D,e,f) and DC(e,f) = M(D,e,f-1) S(N,e,f) and DC(e,f) = W(e,f) 規(guī)格說明簡單形式: 當(dāng)前狀態(tài) and 事件 and 謂詞 =下一個狀態(tài)電梯的 STDM(U,e,f+1)M(D,e,f)S(U,e,f)S(N,e,f)S(D,e,f)M(U,e,f)M(D,e,f-1)W(e,f)ST(e,f)ST(e,f)RLRLDC(e,f)RLRLRLRLRL生產(chǎn)者消費者系統(tǒng)生產(chǎn)者消費者系統(tǒng)u生產(chǎn)者（一個）u生產(chǎn)產(chǎn)品 / 存入倉庫u消費者（一個）u從倉庫取出產(chǎn)品 / 消費產(chǎn)品u倉庫（兩個貨位）u存庫

13、/ 出庫u規(guī)則u如果倉庫是滿的，生產(chǎn)者進(jìn)程必須等待，直到消費者進(jìn)程從倉庫中拿走產(chǎn)品，使倉庫產(chǎn)生一個空的貨位u如果倉庫是空的，消費者進(jìn)程必須等待，直到生產(chǎn)者生產(chǎn)一個產(chǎn)品并存入庫中生產(chǎn)者消費者系統(tǒng)生產(chǎn)者消費者系統(tǒng)三個有限狀態(tài)機(jī)描述),(M11211PPP存庫生產(chǎn))C,C,C(M12212消費出庫)0 ,2 , 1 , 0(M33出庫入庫P1P2生產(chǎn)生產(chǎn)存庫存庫C1C2出庫出庫消費消費0C2入庫入庫出庫出庫12入庫入庫出庫出庫生產(chǎn)者消費者系統(tǒng)生產(chǎn)者消費者系統(tǒng)三個狀態(tài)機(jī)的同步積復(fù)合無定義，其余),(),(),(), ,(),(), (),(, ),(), ,(),(, ),(), (),(, ),()

14、, , (),(, ),(, ),(), , ()a),q,q,q()Qq,q,q(q0QQQQ)q,Q(MMMM3333212223211113213332223213331113212221113213332221113213213020103213210321qaqqqqqaqqqqqaqqqqqaqqaqqqqqaqqaqqqqqaqqaqqqqqaqqaqqaqqqq生產(chǎn)者消費者系統(tǒng)生產(chǎn)者消費者系統(tǒng)0,P1,C10,P2,C1生產(chǎn)1,P1,C1入庫0,P1,C2出庫消費0,P2,C2生產(chǎn)1,P2,C1消費生產(chǎn)1,P2,C22,P2,C22,P2,C12,P1,C11,P1,C22,P

15、1,C2入庫消費生產(chǎn)消費出庫消費生產(chǎn)消費出庫入庫入庫出庫有限狀態(tài)機(jī)系統(tǒng)的局限性有限狀態(tài)機(jī)系統(tǒng)的局限性1. 系統(tǒng)的狀態(tài)數(shù)具有狀態(tài)組合的復(fù)雜性問題2. 在每一個狀態(tài)上，任一時刻最多執(zhí)行一個操作，只能描述順序系統(tǒng)，不能描述并發(fā)系統(tǒng)3. 不能描述無限狀態(tài)系統(tǒng)，缺乏描述時間特性的機(jī)制uPetri 的特點 (1) Petri 網(wǎng)是一種數(shù)學(xué)工具和圖形工具 (2) Petri 網(wǎng)可用于描述系統(tǒng)的不同層次的抽象 (3) Petri 網(wǎng)可用于描述系統(tǒng)的事件之間因果相關(guān)性和不相關(guān)性uPetri 網(wǎng)基本概念 簡稱PNG (Petri Net Graph)是一種有向圖, 有兩種結(jié)點:表示狀態(tài)及狀態(tài)變化u可用三元組N=(

16、P,T,F)表示u位置（Place）或稱庫所集（Places）,符號為 ,表示系統(tǒng)的狀態(tài)u轉(zhuǎn)移（Transition）或稱變遷,符號為“”或者“|” 表示系統(tǒng)中的事件u符號“ ”庫所指向變遷，表示事件發(fā)生的前提，即對變遷的輸入u符號“ ”從變遷指向庫所，表示事件的結(jié)果，即由變遷的輸出u標(biāo)記（token）或稱令牌，符號為 u點燃（fire）符號為u使能的(enabled) :變遷可以被點燃.1t2t3t4t5t6t1P2P4P3P5P6P7P1P4P2P3P5P1t2t3t4tPetri網(wǎng)圖網(wǎng)圖標(biāo)記出現(xiàn)，事件標(biāo)記出現(xiàn)，事件t3 激發(fā)的兩個前提已具備，激發(fā)的兩個前提已具備，事件事件t3激發(fā)激發(fā),P

17、3,P5 的標(biāo)記移到的標(biāo)記移到P4上上定義一：一個Petri網(wǎng)是一個五元組，PN= P,T,A,W,M0 ,其中：,21nPPPP是一個庫所（Place）集P對各弧賦權(quán)值,21mtttT是一個變遷（transition）集T)()(PTTPA是一個有向弧集，（P,T,A）構(gòu)成一個有向圖0:NAW,002010nuuuM是一個初始標(biāo)記（initial marking）標(biāo)記用M表示， 看成是從庫所到自然數(shù)N的一個映射NPM:如果niuPMii, 2 , 1,)(，則說庫所 中有 個令牌（token）iuiP可看成向量，其第 個分量 表示 賦給 的令牌個數(shù)Mi)(iPMMiP定義二：定義二：一個變遷

18、的輸入庫所集為：一個變遷的輸入庫所集為：),( |)(:AtPPtITt 簡記簡記t *定義三定義三：一個變遷的輸出庫所集為：一個變遷的輸出庫所集為：), ( |)(:APtPtOTt簡記簡記* t定義四：定義四：如果如果),()(: )(tPWPMtIP則變遷則變遷 說成是說成是 使能的使能的 tMPetri 網(wǎng)的基本形式化定義網(wǎng)的基本形式化定義Petri 網(wǎng)的執(zhí)行規(guī)則網(wǎng)的執(zhí)行規(guī)則p沖突(Confict)：兩個使能變遷,若點燃其中一個,使另一個變遷變成不使能的p不確定性 (Nondeterminism)：若同時有多個變遷使能,可以點燃其中任意一個(但不確定)p餓死: 一個進(jìn)程從未得到所需要的

19、資源p死鎖:兩個流需要的資源都被對方占有p活動狀態(tài):在給定標(biāo)記情況下, 執(zhí)行不處于死鎖狀態(tài)1t1t2t3t4t5t6t1P2P4P3P5P6P7P初始令牌初始令牌, , 都是使能的都是使能的2t1t1P4P2t2P5P點燃點燃 但但 還是還是使能的使能的,可可以被點燃以被點燃1t2t點燃點燃 但但 還是還是使能的使能的,可可以被點燃以被點燃1t2tpetri 網(wǎng)的活動狀態(tài)網(wǎng)的活動狀態(tài)1t2t3t4t5t6t1P2P4P3P5P6P7P 和和 都是使能的都是使能的, ,哪一個被點燃是不確哪一個被點燃是不確定的定的. . 若點燃變遷若點燃變遷 , , 就不是使能的就不是使能的, ,或反之或反之.

20、.4t3t4t3tPetri網(wǎng)的活動狀態(tài)網(wǎng)的活動狀態(tài)1t2t3t4t1P2P3P在在 庫所中增加一個庫所中增加一個資源拷貝。這樣有兩個資資源拷貝。這樣有兩個資源可以被系統(tǒng)等到源可以被系統(tǒng)等到, , 不會發(fā)生沖突不會發(fā)生沖突和資源競爭和資源競爭,而是可以并而是可以并行執(zhí)行行執(zhí)行3P3t4t解決沖突的解決沖突的Petri網(wǎng)模型網(wǎng)模型易出現(xiàn)死鎖易出現(xiàn)死鎖解決死鎖的解決死鎖的Petri網(wǎng)網(wǎng) (1)用Petri網(wǎng)模擬有限狀態(tài)機(jī) 例 自動面包機(jī)系統(tǒng) 售貨機(jī)接收硬幣面值是0.5元和1.0元 面包價格是1.5元和2.0元 售貨機(jī)最大硬幣存儲是2.0元Petri 網(wǎng)的應(yīng)用網(wǎng)的應(yīng)用自動面包售貨機(jī)系統(tǒng)自動面包售貨機(jī)

21、系統(tǒng)1.5 元元1t2t3t1P2P3P4t4P5P t2和t3是并發(fā)關(guān)系,并發(fā)可以看作是一種二元關(guān)系因果關(guān)系獨立，一個轉(zhuǎn)移可以先于、后于或同時于另一個轉(zhuǎn)移(2) 并發(fā)活動并發(fā)活動1t2t(3) 數(shù)據(jù)流計算數(shù)據(jù)流計算(4) 通信協(xié)議通信協(xié)議1t2t3t1P2P3P4t4P1P3P2P4P:進(jìn)程處于就緒狀態(tài)進(jìn)程處于就緒狀態(tài) :讀進(jìn)程讀進(jìn)程:資源允許進(jìn)程訪問資源允許進(jìn)程訪問 :寫進(jìn)程寫進(jìn)程(5) 同步控制同步控制1t3t1P2P3P4t4P5P2t生產(chǎn)者生產(chǎn)者/消費者的消費者的Petri網(wǎng)模型網(wǎng)模型生產(chǎn)者處生產(chǎn)者處于就緒于就緒生產(chǎn)者生產(chǎn)者正在生正在生產(chǎn)產(chǎn)品產(chǎn)產(chǎn)品消費者消費者處于就緒處于就緒消費者消

22、費者正在消正在消費費產(chǎn)品產(chǎn)品倉庫倉庫p 可達(dá)樹是有向圖，給定某一狀態(tài)v , 從初始狀態(tài)V0到狀態(tài) v，有沒有狀態(tài)推移序列，用可達(dá)樹進(jìn)行檢查p 某一時刻狀態(tài)用n元組(M1,M2,Mn) 表示，Mi代表第i個庫所具有的令牌數(shù)Petri 網(wǎng)的可達(dá)樹表示網(wǎng)的可達(dá)樹表示1t3t1P2P3P4t4P5P2t5t6P7P6t進(jìn)程同步進(jìn)程同步Petri網(wǎng)網(wǎng))0001010(，) 1001100(，激發(fā)激發(fā)) 1001001 (，)0010100(，激發(fā)激發(fā)激發(fā)激發(fā)) 0001010 (，)0010001 (，激發(fā)激發(fā)激發(fā)激發(fā)) 1100100(，激發(fā)激發(fā)) 1100001 (，激發(fā)激發(fā)) 1001001 (，

23、激發(fā)激發(fā)激發(fā)激發(fā))0100010(，) 1100100(，激發(fā)激發(fā)激發(fā)激發(fā))0001010(，) 1001100(，激發(fā)激發(fā)激發(fā)激發(fā)) 1100001 (，)0010100(，激發(fā)激發(fā)激發(fā)激發(fā)) 1001001 (，1t3t4t2t5t6t1t3t4t2t5t6t3t5t6t可達(dá)樹可達(dá)樹當(dāng)前系統(tǒng)狀態(tài)當(dāng)前系統(tǒng)狀態(tài)從從Petri 網(wǎng)到程序結(jié)構(gòu)的轉(zhuǎn)換網(wǎng)到程序結(jié)構(gòu)的轉(zhuǎn)換庫所代替庫所代替聯(lián)接孤聯(lián)接孤變遷代替變遷代替從從Petri 網(wǎng)到程序結(jié)構(gòu)的轉(zhuǎn)換網(wǎng)到程序結(jié)構(gòu)的轉(zhuǎn)換Z方法簡介方法簡介uZ的集合理論和一階謂詞邏輯支持?jǐn)?shù)據(jù)抽象(表示抽象)和過程抽象（操作抽象）u通過表示抽象，數(shù)據(jù)從數(shù)據(jù)結(jié)構(gòu)的表示細(xì)節(jié)抽象出來

24、，使用關(guān)系、函數(shù)、序列、集合等抽象的數(shù)據(jù)類型，構(gòu)成Z語言的類型系統(tǒng)，通過類型定義、全局常（變）量以及狀態(tài)空間聲明進(jìn)行表述u操作抽象描述了在數(shù)據(jù)抽象中所引入的數(shù)據(jù)上的抽象算法與操作，通過函數(shù)和基于一階謂詞邏輯的操作來表述關(guān)于關(guān)于Z的模式的模式u模式（Schema）是Z的基本描述單位，軟件系統(tǒng)的Z描述主要由若干模式構(gòu)成，通過模式刻畫系統(tǒng)的靜態(tài)特性和動態(tài)行為u狀態(tài)模式：定義目標(biāo)軟件系統(tǒng)某一部分的狀態(tài)空間及其約束特性，通過抽象變量以及一些約束關(guān)系來表述u操作模式：描述系統(tǒng)某部分的行為特征，通過描述操作前的狀態(tài)值和操作后的狀態(tài)值之間的關(guān)系來定義系統(tǒng)的操作特性u每個模式均包括一個聲明部分和一個斷言部分（謂

25、詞部分），聲明部分引入變量，斷言部分描述變量之間的關(guān)系u通過簡單模式可以構(gòu)造復(fù)雜模式Z文檔結(jié)構(gòu)（文檔結(jié)構(gòu)（Z的基本組成）的基本組成）（1）給定狀態(tài)聲明和全局變量的定義（2）系統(tǒng)抽象狀態(tài)描述：使用狀態(tài)模式描述系統(tǒng)的狀態(tài)空間和約束特性（3）系統(tǒng)初始化定義，給出初始狀態(tài)（4）對正常條件下系統(tǒng)操作的定義（5）定義操作的前置條件（6）描述完整的操作，包括非正常情況下的操作（7）對規(guī)格說明的一些性質(zhì)的證明（8）建立規(guī)格說明的摘要和目錄u給定集合、數(shù)據(jù)類型和常量u狀態(tài)定義u初始狀態(tài)u操作 組成組成:(1) 給定集合(given set) Button 是所有按鈕的集合(2) 狀態(tài)定義 由模式(schema)

26、組成聲明聲明謂詞謂詞Z模式模式:電梯中的Button子集:樓層按鈕,電梯按鈕按鈕集合buttons被按下按鈕集合pushedfloor_buttons elevator_buttons=floor_buttons elevator_buttons=buttons floor_buttons, elevator_buttons :p Button buttons :p Button pushed :p Button抽象初始狀態(tài)抽象初始狀態(tài): Button_Init = Button_ = 電梯的全部按鈕關(guān)閉電梯的全部按鈕關(guān)閉 Statepushed (4) 操作操作 按下某按鈕,若開啟,將該按鈕

27、加入pushed集合圖書館數(shù)據(jù)庫管理系統(tǒng)圖書館數(shù)據(jù)庫管理系統(tǒng)PART2：問題簡介問題簡介u需求描述（1）圖書副本（copy）的借出與歸還（2）從書庫（stock）中去除圖書復(fù)本或向書庫中添加圖書復(fù)本（3）通過圖書作者或主題查詢圖書信息（4）查詢某讀者借書信息（5）查詢某圖書當(dāng)前被哪位讀者借閱問題簡介問題簡介u系統(tǒng)用戶（兩類）u圖書管理人員（staff）:可進(jìn)行事務(wù)（1）（2）（4）（5）的操作u普通讀者（borrowers）可以進(jìn)行事務(wù)（3）的操作；用事務(wù)（4）列出他自己的借書信息 問題簡介問題簡介u其它約束u書庫內(nèi)的任何圖書復(fù)本要么已借出,要么可以借出u不存在某圖書復(fù)本既可以被借出又已借出u

28、讀者能夠借閱圖書的總數(shù)不能超過給定的限值給定類型和枚舉類型給定類型和枚舉類型u規(guī)格說明使用以下給定類型 PERSON,COPY,TITLE,AUTHOR,SUBJECTuPERSON是所有可能的人的集合uCOPY是所有可能的復(fù)本以后還會產(chǎn)生新的復(fù)本的集合，書是抽象的對象，而復(fù)本則是具體的對象uTITLE是所有可能的書名的集合uAUTHOR是所有可能的作者的集合，與PERSON有區(qū)別，因為有些書是由某個團(tuán)體編寫的uSUBJECT是所有可能的主題的集合給定類型和枚舉類型給定類型和枚舉類型u注：為了處理圖書館中可能含有同一本書的不同復(fù)本的可能性，把圖書和圖書副本加以區(qū)別u增加一個特定的類型REPOR

29、T，代表所有必要信息的集合uREPORT:=unknown librarian | unknown browser |too many books | book not in stock |book not available | book not check out | book in stock | book never out | unknown user | oku還需要一個常數(shù)maxbooks,表示作者最多可借的復(fù)本的數(shù)目抽象規(guī)格說明抽象規(guī)格說明u用戶需求的形式化u系統(tǒng)的兩類用戶（staff和borrowers）不重合borrowersstaffPERSONPborrowersPER

30、SONPstaff:抽象規(guī)格說明（續(xù)）抽象規(guī)格說明（續(xù)）u對于圖書館的書庫，有如下三種需求需要滿足:（1）書庫（stock）中所有的圖書復(fù)本都可以借閱或已借出u其中：available是當(dāng)前書庫中可外借的圖書復(fù)本的集合； checked_out是圖書的借出記錄，它以圖書復(fù)本到用戶的部分函數(shù)形式表現(xiàn)出來stockavailable)out_checkeddom(PERSONCOPY:out_checkedCOPYP:availableCOPYP:stock抽象規(guī)格說明（續(xù)）抽象規(guī)格說明（續(xù)）（2）書庫中的圖書復(fù)本不可能既已借出還能外借，有如下謂詞：（3）讀者所借閱圖書總數(shù)不能超過maxbooks

31、，有如下謂詞：u由常識可知,只有本系統(tǒng)的用戶(管理人員和普通讀者)才能借書:availableoutcheckeddom)_(bookspoutcheckedPERSONpNbooksmax)_(#:maxborrowersstaffoutcheckedran_抽象規(guī)格說明（續(xù)）抽象規(guī)格說明（續(xù)）u從事務(wù)（5）需求可知，系統(tǒng)中應(yīng)該記錄最后借閱某圖書復(fù)本的讀者：PERSONCOPYoutcheckedlast:_u若某人當(dāng)前借閱了某本書，他必定是該書最后借閱的讀者，有下列不變式成立：outcheckedlastoutchecked_抽象規(guī)格說明（續(xù)）抽象規(guī)格說明（續(xù)）u模式BOOK定義了圖書信息

32、BOOKSUBJECTF:subjectsAUTHORF:authorsTITLE:titleu圖書復(fù)本的有關(guān)信息采用從圖書復(fù)本到圖書的部分函數(shù)表示stockoinf_bookdomBOOKCOPY:oinf_book狀態(tài)模式狀態(tài)模式u模式USER-用戶狀態(tài)模式USERSPERSONP:borrowersPERSONP:staffborrowersstaff狀態(tài)模式狀態(tài)模式uDB是書庫和借閱信息的數(shù)據(jù)庫狀態(tài)模式DBBOOKCOPY:oinf_bookPERSONCOPY:out_checked_lastPERSONCOPY:out_checkedCOPYP:availableCOPYP:sto

33、ckstockoinf_bookdomout_checked_lastout_checkedbooksmax)pout_checked(#PERSON:pavailable)out_checkeddom(stockavailable)out_checkeddom(狀態(tài)模式狀態(tài)模式uLIB是由USER和DB組成的狀態(tài)模式LIBDBUSERSborrowersstaffout_checkedran狀態(tài)模式狀態(tài)模式u其它模式：BOOK, USER, DB, LIB和BOOK, USER, DB, LIBLIBLIBLIBDBDBDBUSERUSERUSERBOOKBOOKBOOKDBDBUSERSU

34、SERS|LIBLIBoinf_book oinf_bookout_checked_lastout_checked_lastout_checkedout_checkedavailableavailablestockstock|DBDBborrowersborrowersstaffstaff|USERUSERsubjectssubjectsauthorsauthorstitletitle|BOOKBOOK初始狀態(tài)模式初始狀態(tài)模式u系統(tǒng)初始時，書庫中無圖書及圖書復(fù)本，也無借出記錄，至少存在一個管理人員out_checked_lastout_checkedavailable oinf_booksto

35、ck| DBInitDBstaff| USERSInitUSERSInitDBInitUSERS| LIBInitLIB管理人員事務(wù)管理人員事務(wù)u管理人員事務(wù)包括：柜臺事務(wù)、書庫事務(wù)和查詢事務(wù)。需要輸入管理人員的名稱，不影響用戶系統(tǒng)，首先引入模式Staff_transStaff_transPERSON:?idLIB?USERSUSERSstaffid管理人員事務(wù)管理人員事務(wù)（1）柜臺事務(wù)Counter_trans：包括圖書借閱事務(wù)和圖書歸還事務(wù)，都需要輸入圖書復(fù)本的標(biāo)識(copy?)，且不影響書庫stockCounter_transCOPY:?copytrans_Staffoinf_book

36、oinf_bookstockstockstock?copy管理人員事務(wù)管理人員事務(wù)u圖書借閱事務(wù)所接受的輸入圖書復(fù)本必須是可借閱的，該事務(wù)更新checked_out記錄和last_checked_out，用如下模式描述：Check_outPERSON:?borrowertrans_Counter?_?_?max?)_(#?borrowercopyoutcheckedlastoutcheckedlastborrowercopyoutcheckedtoucheckedcopyavailableavailablebooksborrowersoutcheckedborrowersstaffborrow

37、eravailablecopy管理人員事務(wù)管理人員事務(wù)u圖書歸還事務(wù)所處理的圖書復(fù)本必須是已經(jīng)借出的書，該事務(wù)也更新checked_out記錄，用模式Return表示：Returntrans_Counterout_checked_lastout_checked_lastout_checked?copyout_checked?copyavailableavailableout_checkeddom?copy管理人員事務(wù)管理人員事務(wù)（2）書庫事務(wù)：包括圖書的添加和去除，都與一書名有關(guān)，但不影響當(dāng)前的借出記錄checked_outStock_transCOPY:?copytrans_Staffout

38、_checkedout_checked管理人員事務(wù)管理人員事務(wù)u圖書添加事務(wù)需要先給定圖書復(fù)本標(biāo)識copy?，并提供書名、作者、主題信息。copy?事先并不在書庫中，加入后馬上可借出AddSUBJECTF:?subjectAUTHORF:?authorsTITLE:?titletrans_Stock?subjectssubjects.B?authorsauthors.B?titletitle.B|BOOK:BwhereB?copyoinf_book oinf_bookout_checked_lastout_checked_last?copyavailableavailable?copystoc

39、kstockstock?copy管理人員事務(wù)管理人員事務(wù)u圖書去除事務(wù)必須保證該圖書復(fù)本正在書庫中，需要更改available記錄和last_checked_out記錄以及book_info。Removetrans_Stockoinf_book?copy oinf_bookout_checked_last?copyout_checked_last?copyavailableavailable?copystockstockstock?copy管理人員事務(wù)管理人員事務(wù)（3）管理人員查詢事務(wù)：不影響各種借書及存書記錄的狀態(tài)Borrowered_list)BOOKCOPY(F: !listPERSON

40、:?borrowertrans_StaffDBDB)c (oinf_book, c (?borrower) c (out_checked|COPY:c!listborrowersstaff?borrower管理人員事務(wù)管理人員事務(wù)u操作模式Last_borrower用于查詢特定圖書復(fù)本現(xiàn)在被哪個讀者借閱，borrower!給出了借閱copy?的讀者Last_borrowerPERSON: !borrowerCOPY:?copytrans_StaffDBDB?)copy(out_checked_last!borrower讀者事務(wù)讀者事務(wù)u普通人員和管理人員可以通過作者或主題信息查詢圖書，普通讀者

41、也可以查詢本人所借閱的圖書，這些事務(wù)均不影響借書記錄checked_out和書庫記錄stockUser_transPERSON:?idLIBLIBLIBborrowersstaff:?id讀者事務(wù)讀者事務(wù)u為查詢方便，應(yīng)給定描述信息與圖書作者信息以及描述信息與主題信息的對應(yīng)關(guān)系DESCSUBJECTDESC:match_SAUTHORDESC:match_Au讀者可以通過作者信息描述查詢圖書讀者事務(wù)讀者事務(wù)Author_enquiryBOOKP: !listDESC:?dtrans_User)|)?d(|match_Aauthors. b(oinf_bookranb|BOOK:b!listu同

42、樣，讀者可以提供主題信息描述查詢圖書讀者事務(wù)讀者事務(wù)Subject_enquiryBOOKP: !listDESC:?dtrans_User)|)?d(|match_Ssubjects. b(oinf_bookranb|BOOK:b!listu讀者也可以查詢他本人所借閱的圖書的信息讀者事務(wù)讀者事務(wù)Self_borrowed_listBOOKP: !listtrans_User)c (oinf_book?id) c (out_checked|COPY:c!listu一個操作的完整描述是由前置條件成立時事務(wù)成功的操作和前置條件不成立時出錯處理的各個部分組成的，首先描述事務(wù)成功時的前置條件：Pre_

43、Check_out給出借書操作的前置條件操作模式的前置條件操作模式的前置條件Pre_Check_outCOPY:?copyPERSON:?borrower?,id;LIBbooksmax?)borrowerout_checked(#available?copyborrowersstaff?borrowerstaff?id操作模式的前置條件操作模式的前置條件Pre_ReturnCOPY:?copyPERSON:?id;LIBout_checkeddom?copystaff?idPre_AddSUBJECTF:?subjectsAUTHORF:?authorsTITLE:?titleCOPY:?c

44、opyPERSON:?id;LIBstock?copystaff?id操作模式的前置條件操作模式的前置條件Pre_RemoveCOPY:?copyPERSON:?id;LIBavailable?copystaff?idPre_Borrower_listPERSON:?borrower?,id;LIBborrowersstaff?borrowerstaff?id操作模式的前置條件操作模式的前置條件Pre_Last_borrowerCOPY:?copyPERSON:?id;LIBout_checked_lastdom?copystaff?idPre_Author_enquiryDESC:?dPER

45、SON:?id;LIBborrowersstaff?id操作模式的前置條件操作模式的前置條件Pre_Subject_enquiryDESC:?dPERSON:?id;LIBborrowersstaff?idPre_Self_borrowed_listPERSON:?id;LIBborrowersstaff?id操作的完整描述和出錯處理操作的完整描述和出錯處理ErrorREPORT: ! rLIBLIBLIBu若操作的前置條件不成立，需要進(jìn)行出錯處理，出錯情況的基本模式及成功時的模式分別表示為：SuccessREPORT: !repOK!rep 操作的完整描述和出錯處理操作的完整描述和出錯處理U

46、nknown librarianPERSON:?idERRORlibrarianunknown! rstaff?idUnknown borrowerPERSON:?borrowerERRORborrowerunknown! rborrowersstaff?borrower操作的完整描述和出錯處理操作的完整描述和出錯處理Too_many_booksPERSON:?borrowerERRORbooksmanytoo! rbooksmax?)borrowerout_checked(#u對于圖書復(fù)本不在書庫中的情況，定義如下出錯處理模式：COPY?copy;ErrorBerror 操作的完整描述和出錯

47、處理操作的完整描述和出錯處理Book_not_availableBerror) availablenotbook! ravailablestock?copy() stockinnotbook! rstock?copy(u圖書借閱事務(wù)的完整操作可用以下模式描述：books_many_tooavailable_not_bookborrower_Unknownlibrarian_Unknown)Successout_Check(out_Check_T操作的完整描述和出錯處理操作的完整描述和出錯處理Book_not_check_outBerror) outcheckednotbook! ravaila

48、ble?copy() stockinnotbook! rstock?copy(u圖書歸還事務(wù)的完整操作可用以下模式描述：out_checked_not_booklibrarian_Unknown)Successturn(ReturnRe_Tu圖書歸還事務(wù)必須考慮圖書未加入書庫或未借出的情況：操作的完整描述和出錯處理操作的完整描述和出錯處理u對于添加圖書操作，若該圖書已經(jīng)在書庫中，則需要進(jìn)行出錯處理，對于圖書復(fù)本在書庫中的情況，可用以下模式描述： stockinbook! rstock?copy|Berrorstock_in_Bookstock_in_booklibrarian_Unknown)

49、SuccessAdd(Add_Tu添加圖書操作的完整描述為：操作的完整描述和出錯處理操作的完整描述和出錯處理u查詢某個讀者借閱圖書信息的操作可描述為：borrower_Unknownlibrarian_Unknown)Successlist_Borrowed(list_Borrowed_Tu去除圖書復(fù)本的完整描述為：available_not_booklibrarian_Unknown)Successmove(RemoveRe_T操作的完整描述和出錯處理操作的完整描述和出錯處理Book_never_outBerror) outneverbook! rout_checked_lastdomsto

50、ck?copy() stockinnotbook! rstock?copy(u查詢特定圖書復(fù)本現(xiàn)在被哪個讀者借閱的操作可描述為：out_never_booklibrarian_Unknown)Successborrower_Last(borrower_Last_Tu查詢特定圖書復(fù)本現(xiàn)在被哪個讀者借閱時的出錯情況可描述為:操作的完整描述和出錯處理操作的完整描述和出錯處理Unknown_userPERSON:?idError) userunknown! rborrowersstaff?idu當(dāng)讀者操作的用戶是未知用戶時，需要進(jìn)行出錯處理，相應(yīng)的模式Unknown_User定義為：操作的完整描述和出

51、錯處理操作的完整描述和出錯處理u通過作者信息描述查詢圖書操作的完整描述可定義為：user_Unknown)Successenquiry_Author(enquiry_Author_Tuser_Unknown)Successenquiry_Subject(enquiry_Subject_Tuser_Unknown)Successlist_borrowed_Self(list_borrowed_Self_Tu通過主題信息描述查詢圖書操作的完整描述可定義為：u讀者查詢本人借閱圖書信息操作的完整描述可定義為：PART3：實際事物形式化方法形式化描述形式化的抽象形式化的抽象p計算和預(yù)測p分析和評估p精準(zhǔn)

52、描述p 軟件體系結(jié)構(gòu)和軟件體系結(jié)構(gòu)描述屬于不同的概念p軟件體系結(jié)構(gòu)附屬于系統(tǒng)之中。只要存在系統(tǒng)，體系結(jié)構(gòu)就存在p如：每個石頭都會有重量p軟件體系結(jié)構(gòu)描述是將體系結(jié)構(gòu)可視化的手段和產(chǎn)物p如：表示一個石頭的重量形式化的描述形式化的描述軟件體系結(jié)構(gòu)軟件體系結(jié)構(gòu)描述如何理解軟件體系結(jié)構(gòu)描述如何理解軟件體系結(jié)構(gòu)描述p 使用不同的策略和方法可對同一軟件體系結(jié)構(gòu)作不同的理解和描述 如：描述一塊石頭的重量 比較輕 比另一塊重一些 大約2公斤 四斤六兩 2.32Kg 5.114751207磅 精確程度不同單位不同測量基準(zhǔn)不同體系結(jié)構(gòu)的描述方式體系結(jié)構(gòu)的描述方式p 體系結(jié)構(gòu)描述方式標(biāo)準(zhǔn) 語義豐富性 語義精確性 形

53、式化程度p 主要描述方式 非標(biāo)準(zhǔn)的圖形符號 UML 模塊接口語言MIL ADLRichnessPrecisenessFormalizationO體系結(jié)構(gòu)的描述方式體系結(jié)構(gòu)的描述方式p 非標(biāo)準(zhǔn)圖形符號描述 用由矩形框和有向線段組合而成的圖形表達(dá)工具。其中，矩形框代表抽象構(gòu)件，有向線段代表輔助各構(gòu)件進(jìn)行通訊、控制或關(guān)聯(lián)的連接件 p 特點 語義豐富 語義極不精確 沒有形式化基礎(chǔ)p 用途 商業(yè)展示 設(shè)計草圖非標(biāo)準(zhǔn)圖形符號描述非標(biāo)準(zhǔn)圖形符號描述非標(biāo)準(zhǔn)圖形符號描述實例非標(biāo)準(zhǔn)圖形符號描述實例-EJB架構(gòu)架構(gòu)p MIL (Module & Interface Language) 是將一種或多種傳統(tǒng)程序

54、設(shè)計語言模塊連接起來描述軟件的體系結(jié)構(gòu)的方法p 特點 語義比較豐富，但局限在實現(xiàn)級別，層次較低 語義精確，有編譯器作保證 沒有或極少有形式化基礎(chǔ)p 實例 Microsoft COM IDL OMG CORBA IDL模塊接口語言模塊接口語言MILp 為什么需要形式化描述 需要嚴(yán)格、精確無歧義的描述 需要具備演算的能力，使得在判斷系統(tǒng)質(zhì)量的時候可以由計算得出，而不是僅僅憑借經(jīng)驗推測 需要進(jìn)行體系結(jié)構(gòu)分析自動化軟件體系結(jié)構(gòu)的形式化描述軟件體系結(jié)構(gòu)的形式化描述軟件系統(tǒng)關(guān)注結(jié)構(gòu)和約束體系結(jié)構(gòu)形式化模型1集合論、謂詞邏輯關(guān)注行為體系結(jié)構(gòu)形式化模型2進(jìn)程代數(shù)形式化方法過程形式化方法過程p 一階謂詞邏輯（F

55、irst Order Predicate Logic）p 集合論p 屬性文法（Attribute Grammar）p 進(jìn)程代數(shù) （Process Algebra） 通訊順序進(jìn)程（CSP，Communicating Sequential Processes） -演算（-Calculus）p Petri網(wǎng)p 狀態(tài)機(jī)（State Machine）p 軟件體系結(jié)構(gòu)的形式化基礎(chǔ)軟件體系結(jié)構(gòu)的形式化基礎(chǔ)p 純形式化方法的不足 形式化方法不能直接支持軟件的各種概念，難以在實踐中應(yīng)用p 體系結(jié)構(gòu)描述語言ADL (Architecture Description Language) 用通用的形式化方法對體系結(jié)構(gòu)

56、和風(fēng)格進(jìn)行建模和分析，在體系結(jié)構(gòu)的抽象級上提供一個精確的語義 提供了強有力的分析能力、抽象和與實現(xiàn)的細(xì)節(jié)無關(guān)性 為體系結(jié)構(gòu)元素定義了一系列符號，可以應(yīng)用于實際的復(fù)雜系統(tǒng)的描述 形式化方法的進(jìn)化形式化方法的進(jìn)化-ADLp 定義和描述體系結(jié)構(gòu)p 描述一個系統(tǒng)是如何被構(gòu)件建立起來的p 描述如何通過現(xiàn)有的構(gòu)件生成新的系統(tǒng)p 指導(dǎo)從多個不同的設(shè)計和實現(xiàn)中挑選最優(yōu)方案p 檢驗一個設(shè)計是否能夠滿足需求p 檢測一個需求對系統(tǒng)的隱含影響p 根據(jù)需求自動化構(gòu)建系統(tǒng)ADL應(yīng)當(dāng)有什么功能應(yīng)當(dāng)有什么功能p ADL在充分繼承和吸收傳統(tǒng)程序設(shè)計語言的精確性和嚴(yán)格性特點的同時，還具有構(gòu)造、抽象、重用、組合、異構(gòu)、分析和推理等

57、各種能力ADL與其它語言的比較與其它語言的比較p 構(gòu)造能力：允許用較小的體系結(jié)構(gòu)元素建造大型軟件系統(tǒng)p 抽象能力：構(gòu)件和連接件的描述可只關(guān)注其抽象特性p 重用能力：所有部件可成為可重用部件p 組合能力：支持軟件系統(tǒng)的動態(tài)變化組合p 異構(gòu)能力：允許多個不同的體系結(jié)構(gòu)描述關(guān)聯(lián)存在p 分析和推理能力：允許對描述的體系結(jié)構(gòu)進(jìn)行多種不同性能和功能上的多種推理分析p 構(gòu)件p 是一個計算單元或數(shù)據(jù)存儲。構(gòu)件是計算與狀態(tài)存在的場所p 包含多種屬性，如接口、類型、語義、約束、演化和非功能屬性p 連接件p 是用來建立構(gòu)件之間交互以及支配這些交互規(guī)則的體系結(jié)構(gòu)構(gòu)造模塊p 體系結(jié)構(gòu)配置p 是描述體系結(jié)構(gòu)的構(gòu)件和連接件

58、的連接圖ADL的構(gòu)成要素的構(gòu)成要素p 根據(jù)研究范圍分類 研究體系結(jié)構(gòu)配置結(jié)構(gòu)的描述語言如Darwin 研究體系結(jié)構(gòu)實例的描述語言如Rapide、UniCon 研究體系結(jié)構(gòu)風(fēng)格的描述語言如WRIGHT、Aesopp 根據(jù)與實現(xiàn)細(xì)節(jié)的關(guān)系的描述語言 實現(xiàn)無關(guān)語言（Implementation Independent Languages） 實現(xiàn)相關(guān)語言（Implementation Constraining Languages）ADL的分類的分類OOADLOOADLDSADL DSADL XYZ/ADLXYZ/ADLrightright系統(tǒng)系統(tǒng)DarwinDarwin系統(tǒng)系統(tǒng)形式化形式化ADLADL

59、幾種幾種ADL簡介簡介p Darwin描述的軟件系統(tǒng)配置主要由構(gòu)件及構(gòu)件之間的綁定組成。構(gòu)件用服務(wù)進(jìn)行定義，構(gòu)件既能對外提供服務(wù)，也能請求外部服務(wù)。所有的服務(wù)名的作用范圍僅限于定義這些服務(wù)的構(gòu)件p Darwin可便于描述系統(tǒng)的動態(tài)特性，采用演算可分析、描述帶有演化通信結(jié)構(gòu)的并發(fā)系統(tǒng)。Darwin使用演算作為其形式化基礎(chǔ)，使用Darwin描述的體系結(jié)構(gòu)模型能夠進(jìn)行一些高層的模型檢測，例如是否存在死鎖等p 在演算中，一個系統(tǒng)被表述成一組具有獨立功能的進(jìn)程集，集合中的每個進(jìn)程可以與其它進(jìn)程建立連接，每個連接都有一個連接名p Darwin采用演算對系統(tǒng)行為進(jìn)行建模，利用其強類型系統(tǒng)進(jìn)行靜態(tài)檢查幾種幾種

60、ADL簡介簡介-Darwinp 針對國內(nèi)唐稚松院士提出基于時序邏輯的XYZ語言進(jìn)行擴(kuò)充，用來描述驗證具有實時性、可靠性要求的軟件體系結(jié)構(gòu)p XYZ/ADL是對時序邏輯語言XYZ/E的擴(kuò)充。它可以在統(tǒng)一的時序邏輯框架下描述系統(tǒng)靜態(tài)語義到實現(xiàn)之間不同抽象層次的規(guī)范，便于體系結(jié)構(gòu)的逐步求精描述以及相關(guān)性質(zhì)分析幾種幾種ADL簡介簡介-XYZ/ADLp 采用屬性文法(AG)來形式化描述軟件體系結(jié)構(gòu)p 傳統(tǒng)的屬性文法是在上下文無關(guān)文法G=(VN,VT,P,Z)上附加上下文有關(guān)的屬性和規(guī)則p VN是非終結(jié)符號集；VT是終結(jié)符號集；P是產(chǎn)生式集；Z是開始符號p 假設(shè)G是規(guī)范的上下文無關(guān)文法，P中的產(chǎn)生式為：p: Xp