第7講 形式化說明技術(shù)

第4章形式化說明技術(shù)1什么是形式化說明技術(shù)從廣義上講，形式化方法是指將離散數(shù)學(xué)的方法用于解決軟件工程領(lǐng)域的問題，主要包括建立精確的數(shù)學(xué)模型以及對(duì)模型的分析活動(dòng)。狹義的講，形式化方法是運(yùn)用形式化語(yǔ)言，進(jìn)行形式化的規(guī)格描述、模型推理和驗(yàn)證的方法。就形式化建模而言，形式化表示必須包含一組定義其語(yǔ)法語(yǔ)義的形式化規(guī)則。這些規(guī)則可用于分析給定的表達(dá)式是否符合語(yǔ)法規(guī)定，或證明該表達(dá)式具有某種性質(zhì)。2形式化說明技術(shù)用自然語(yǔ)言描述需求規(guī)格說明，是典型的非形式化方法。用數(shù)據(jù)流圖或ER圖建立模型，是典型的半形式化方法。所謂形式化方法，就是基于數(shù)學(xué)的技術(shù)來描述系統(tǒng)的性質(zhì)的方法。非形式化方法的缺點(diǎn)形式化方法的優(yōu)點(diǎn)3應(yīng)用形式化方法的準(zhǔn)則(1)應(yīng)該選用適當(dāng)?shù)谋硎痉椒ā?2)應(yīng)該形式化，但不要過分形式化。(3)應(yīng)該估算成本。(4)應(yīng)該有形式化方法顧問隨時(shí)提供咨詢。(5)不應(yīng)該放棄傳統(tǒng)的開發(fā)方法。把形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋硎强赡艿?，而且由于取長(zhǎng)補(bǔ)短往往能獲得很好的效果。(6)應(yīng)該建立詳盡的文檔。建議使用自然語(yǔ)言注釋形式化的規(guī)格說明書，以幫助用戶和維護(hù)人員理解系統(tǒng)。(9)應(yīng)該測(cè)試、測(cè)試再測(cè)試。(10)應(yīng)該重用。即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的惟一合理的方法。而且用形式化方法說明的軟件構(gòu)件具有清晰定義的功能和接口，使得它們有更好的可重用性。4有窮狀態(tài)機(jī)例子：保險(xiǎn)箱的復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)記為1，2，3，轉(zhuǎn)盤可向左（L）或向右（R）轉(zhuǎn)動(dòng)。任意時(shí)刻的6種可能的運(yùn)動(dòng)：1R,1L,2R,2L,3R,3L假設(shè)組合密碼為：1L,3R,2L，除了這個(gè)次序的任意轉(zhuǎn)動(dòng)都將導(dǎo)致報(bào)警。保險(xiǎn)箱鎖定AB保險(xiǎn)箱解鎖報(bào)警1L轉(zhuǎn)盤的任何其他移動(dòng)3R2L轉(zhuǎn)盤的任何其他移動(dòng)轉(zhuǎn)盤的任何其他移動(dòng)初始態(tài)終態(tài)終態(tài)5當(dāng)前狀態(tài)次態(tài)轉(zhuǎn)盤動(dòng)作

保險(xiǎn)箱鎖定AB1LA報(bào)警報(bào)警1R報(bào)警報(bào)警報(bào)警2L報(bào)警報(bào)警保險(xiǎn)箱解鎖2R報(bào)警報(bào)警報(bào)警3L報(bào)警報(bào)警報(bào)警3R報(bào)警B報(bào)警狀態(tài)集J：{保險(xiǎn)箱鎖定，A，B，保險(xiǎn)箱解鎖，報(bào)警}。輸入集：{1L，1R，2L，2R，3L，3R}轉(zhuǎn)換函數(shù)：T初始態(tài)S：保險(xiǎn)箱鎖定。終態(tài)集：{保險(xiǎn)箱解鎖，報(bào)警}6一個(gè)有窮狀態(tài)機(jī)可以表示為一個(gè)5元組{J，K，T，S，F(xiàn)}J是一個(gè)有窮的非空狀態(tài)集K是一個(gè)有窮的非空輸入集T是一個(gè)從（J-F）*K到J的轉(zhuǎn)換函數(shù)S∈J，是一個(gè)初始狀態(tài)F

J，是終態(tài)集例如：菜單一個(gè)菜單的顯示和一個(gè)狀態(tài)相對(duì)應(yīng)鍵盤輸入或鼠標(biāo)點(diǎn)擊對(duì)應(yīng)于一個(gè)事件當(dāng)前狀態(tài)[菜單]+事件[所選擇的項(xiàng)]+謂詞=>下個(gè)狀態(tài)7電梯的例子電梯的約束條件：C1：每部電梯有m個(gè)按鈕，每個(gè)按鈕代表一個(gè)樓層。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，同時(shí)電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時(shí)指示燈滅。C2：除了樓的最低層和最高層外，每層樓有兩個(gè)按鈕分別指示是上樓還是下樓。這兩個(gè)按鈕之一被按下時(shí)相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時(shí)燈熄滅，電梯向要求的方向移動(dòng)。C3：當(dāng)對(duì)電梯沒有請(qǐng)求時(shí)，它關(guān)門并停在當(dāng)前樓層。8電梯按鈕EB（e,f）：表示按下電梯e內(nèi)的按鈕并請(qǐng)求到f層去EBP（e,f）:電梯按鈕(e,f)被按下EAF（e,f）:電梯e到達(dá)f層謂詞：V(e,f):電梯停在f層如果電梯按鈕(e,f)處于關(guān)閉狀態(tài)[當(dāng)前狀態(tài)]，而且電梯(e,f)被按下[事件]，而且電梯e不在f層[謂詞]，則該電梯按鈕打開發(fā)光[下個(gè)狀態(tài)]。狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下：EBOFF(e,f)+EBP(e,f)+notV(e,f)=>EBON(e,f)EBON(e,f)+EAF(e,f)=>EBOFF(e,f)EBOFF(e,f)EBON(e,f)EBP(e,f)EAF(e,f)9樓層按鈕FB(d,f)表示f層請(qǐng)求電梯向d方向運(yùn)動(dòng)的按鈕FBON(d,f):樓層按鈕(d,f)打開FBOFF(d,f)：樓層按鈕(d,f)關(guān)閉FBP(d,f):樓層按鈕(d,f)被按下EAF(1…n,f):電梯1或…或n到達(dá)f層S(d,e,f)：電梯e停在f層并且移動(dòng)方向由d確定為向上(d=U)或向下(d=D)或待定(d=N)狀態(tài)轉(zhuǎn)換規(guī)則：FBOFF(d,f)+FBP(d,f)+notS(d,1…n,f)=>FBON(d,f)FBON(d,f)+EAF(1…n,f)+S(d,1…n,f)=>FBOFF(d,f)FBOFF(d,f)FBON(d,f)FBP(d,f)EAF(1…n,f)10V(e,f)=S(U,e,f)orS(D,e,f)orS(N,e,f)電梯的三個(gè)狀態(tài)：M(d,e,f)：電梯e正沿d方向移動(dòng)，即將到達(dá)的是第f層S(d,e,f)：電梯e停在f層，將朝d方向移動(dòng)(尚未關(guān)門)W(e,f):電梯e在f層等待(已關(guān)門)可觸發(fā)狀態(tài)發(fā)生改變的事件DC(e,f):電梯e在樓層f關(guān)上門ST(e,f):電梯e靠近f層時(shí)觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下RL：電梯按鈕或樓層按鈕被按下進(jìn)入打開狀態(tài)，登錄需求電梯的狀態(tài)轉(zhuǎn)換規(guī)則S(U,e,f)+DC(e,f)=>M(U,e,f+1)S(D,e,f)+DC(e,f)=>M(D,e,f-1)S(N,e,f)+DC(e,f)=>W(e,f)11S(U,e,f)S(N,e,f)M(U,e,f+1)S(D,e,f)M(D,e,f)M(U,e,f)M(D,e,f-1)W(e,f)DC(e,f)RLRLST(e,f)RLRLRLDC(e,f)DC(e,f)ST(e,f)12Petri網(wǎng)Petri網(wǎng)是用于形式化說明定時(shí)問題的一種技術(shù)一組位置P為｛P1，P2，P3，P4｝，在圖中用圓圈代表位置。一組轉(zhuǎn)換T為｛t1，t2｝，在圖中用短直線表示轉(zhuǎn)換。兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是： I(t1)=｛P2，P4｝I(t2)=｛P2｝兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是: O(t1)=｛P1｝O(t2)=｛P3，P3｝p1p2p4t2t1p313Petri網(wǎng)包含4種元素：一組位置P、一組轉(zhuǎn)換T、輸入函數(shù)I以及輸出函數(shù)O。Petri網(wǎng)結(jié)構(gòu)，是一個(gè)四元組C=(P,T,I,O)P={P1,…,Pn}是一個(gè)有窮位置集T={t1,…,tm}是一個(gè)有窮轉(zhuǎn)換集I：T->P∞

為輸入函數(shù)，是由轉(zhuǎn)換到位置組的映射O：T->P∞

為輸出函數(shù)，是由轉(zhuǎn)換到位置組的映射14p1p2p4t2t1p3p1p2p4t2t1p3標(biāo)記：(1,2,0,1)標(biāo)記：(2,1,0,0)標(biāo)記：(2,0,2,0)p1p2p4t2t1p3權(quán)標(biāo)15Petri網(wǎng)的標(biāo)記M，是由一組位置P到一組非負(fù)整數(shù)的映射：M：P->{0,1,2……}所以，Petri網(wǎng)成為一個(gè)五元組（P,T,I,O,M）16p1p2p3t1對(duì)Petri網(wǎng)的擴(kuò)充：加入禁止線。禁止線是用一個(gè)圓圈而不是用箭頭標(biāo)記的輸入線。通常。當(dāng)每個(gè)輸入線上至少有一個(gè)權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)的時(shí)候，相應(yīng)的轉(zhuǎn)換才是允許的。17C1:每部電梯有m個(gè)按鈕，每層對(duì)應(yīng)一個(gè)按鈕。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當(dāng)電梯到達(dá)指定的樓層時(shí)，按鈕熄滅。電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示。(1≤f≤m)。在EBf上有一個(gè)權(quán)標(biāo)，表示電梯內(nèi)樓層f的按鈕被按下了。18FgFfEBfEBf被按下電梯在運(yùn)行電梯按鈕只有在第一次被按下時(shí)才會(huì)由暗變亮，以后再按它會(huì)被忽略。假設(shè)按鈕沒有亮，在位置Ebf上沒有權(quán)標(biāo)，那么在存在禁止線的情況下，轉(zhuǎn)換“EBf”是允許發(fā)生的。按下按鈕之后，則轉(zhuǎn)換被激發(fā)并在EBf上放置了一個(gè)權(quán)標(biāo)，以后無論再按下多少次按鈕，禁止線與現(xiàn)有權(quán)標(biāo)的組合都決定了轉(zhuǎn)換“EBf被按下”不能再被激發(fā)了，因此，位置EBf上的權(quán)標(biāo)數(shù)不會(huì)多于119圖4.11Petri網(wǎng)表示樓層按鈕204Z語(yǔ)言簡(jiǎn)介用Z語(yǔ)言描述的、最簡(jiǎn)單的形式化規(guī)格說明含有下述4個(gè)部分：給定的集合、數(shù)據(jù)類型及常數(shù)。狀態(tài)定義。初始狀態(tài)。操作。211.給定的集合一個(gè)Z規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集合用帶方括號(hào)的形式表示。對(duì)于電梯問題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，Z規(guī)格說明開始于：〔Button〕2.狀態(tài)定義一個(gè)Z規(guī)格說明由若干個(gè)“格(schema)”組成，每個(gè)格含有一組變量說明和一系列限定變量取值范圍的謂詞。例如，Z格S的格式如圖4.12所示。22在電梯問題中，Button有4個(gè)子集，floor_buttons(樓層按鈕的集合)elevator_buttons(電梯按鈕的集合)buttons(電梯問題中所有按鈕的集合)pushed(所有被按的按鈕的集合，即所有處于打開狀態(tài)的按鈕的集合)。233.初始狀態(tài)抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時(shí)的狀態(tài)。對(duì)于電梯問題來說，抽象的初始狀態(tài)為：Button_Init〔Button_State｜pushed=Φ〕上式表示，當(dāng)系統(tǒng)首次開啟時(shí)pushed集為空，即所有按鈕都處于關(guān)閉狀態(tài)。4.操作如果一個(gè)原來處于關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個(gè)按鈕就被添加到pushed集中。24△Button_Statebutton?:button(button?∈buttons)∧(((button?∈pushed)∧(pushed’=pushed∪{button?))∨((button?∈pushed)∧(pushed’=pushed)))△Button_Statebutton?:button(button?∈buttons)∧(((button?∈pushed)∧(pushed’=pushed\{button?}))∨((button?∈pushed)∧(pushed’=pushed)))Push_buttonFloor_Arrival’25Z語(yǔ)言實(shí)例：停車場(chǎng)管理系統(tǒng)基本數(shù)據(jù)類型定義–“停車提示”是一個(gè)基本數(shù)據(jù)類型的名字–“停好”和“停車場(chǎng)滿”是該類型的數(shù)據(jù)可能的取值停車提示=停好|停車場(chǎng)滿全局變量聲明 –在Z語(yǔ)言中，N和Z屬于基本數(shù)據(jù)集合，分別表示正整數(shù)集合和整數(shù)集合。停車場(chǎng)容量:Z/*變量聲明*/停車場(chǎng)容量≥0/*變量約束*/26狀態(tài)定義 –每個(gè)系統(tǒng)有唯一的狀態(tài)定義，可以為狀態(tài)命名。本例中為系統(tǒng)狀態(tài)命名為“停車場(chǎng)狀態(tài)”。狀態(tài)定義中首先聲明一或多個(gè)表示系統(tǒng)狀態(tài)的變量，這里的變量名為“停車數(shù)量”，類型為整數(shù)。該變量的約束條件為取值大于等于0，小于等于最大停車數(shù)量。 –停車場(chǎng)狀態(tài)停車數(shù)量:Z/*狀態(tài)變量聲明*/停車數(shù)量≥0停車數(shù)量≤停車場(chǎng)容量27初始化 –定義系統(tǒng)狀態(tài)變量的初始值。系統(tǒng)的初始化定義是唯一的。28操作定義–每個(gè)系統(tǒng)可以定義若干個(gè)操作。–Z語(yǔ)言中操作的定義是基于狀態(tài)的，而不是基于過程的。該操作如何改變了系統(tǒng)的狀態(tài)變量的值？該操作有哪些輸入變量？有哪些輸出變量？–當(dāng)一個(gè)操作改變了某個(gè)系統(tǒng)狀態(tài)變量x時(shí)，在操作定義的第一行寫出狀態(tài)變化聲明Δx。–當(dāng)一個(gè)操作未改變?nèi)魏蜗到y(tǒng)狀態(tài)變量時(shí)，即可以在操作定義第一行寫出以下狀態(tài)聲明Ξ狀態(tài)變量（可省略）。29操作定義（續(xù)）30操作定義也可以采用以下形式進(jìn)入停車場(chǎng)?正常停車∨停車場(chǎng)滿表示： –操作“進(jìn)入停車場(chǎng)”分為“正常停車”和“停車場(chǎng)滿”兩種可能情況，具體執(zhí)行時(shí)選擇哪種情況，由環(huán)境滿足哪種操作的約束條件來決定。31評(píng)價(jià)Z語(yǔ)言優(yōu)勢(shì)：(1)可以比較容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯(cuò)誤，特別是在自己審查規(guī)格說明，及根據(jù)形式化的規(guī)格說明來審查設(shè)計(jì)與代碼時(shí)，情況更是如此。(2)用Z寫規(guī)格說明時(shí)，要求作者十分精確地使用Z說明符。由于對(duì)精確性的要求很高，從而和非形式化規(guī)格說明相比，減少了模糊性、不一致性和遺漏。

(3)Z是一種形式化語(yǔ)言，在需要時(shí)開發(fā)者可以嚴(yán)格地驗(yàn)證規(guī)格說明的正確性。(4)雖然完全學(xué)會(huì)Z語(yǔ)言相當(dāng)困難，但是，經(jīng)驗(yàn)表明，只學(xué)過中學(xué)數(shù)學(xué)的