軟件工程(第3版)第14章人民郵電出版社.ppt

《軟件工程(第3版)第14章人民郵電出版社.ppt》由會(huì)員分享，可在線閱讀，更多相關(guān)《軟件工程(第3版)第14章人民郵電出版社.ppt（121頁(yè)珍藏版）》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。

1、第五篇 高級(jí)課題 第 14章 形式化方法 概述 14.1 有窮狀態(tài)楊 14.2 Petri網(wǎng) 14.3 語(yǔ)言 14.4 小結(jié) 14.5 根據(jù)形式化的程度，可以把軟件工程 方法劃分成非形式化、半形式化和形式化 三類。使用自然語(yǔ)言描述需求規(guī)格說(shuō)明， 是典型的非形式化方法。使用數(shù)據(jù)流圖或 實(shí)體 關(guān)系圖等圖形符號(hào)建立模型，是典型 用于開發(fā)計(jì)算機(jī)系統(tǒng)的形式化方法， 是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)，也就 是說(shuō)，如果一 個(gè)方法有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)， 那么它就是形式化的。 14.1 概述 14.1.1 非形式化方法的缺點(diǎn) 基本上使用自然語(yǔ)言描述的系統(tǒng)規(guī)格 說(shuō)明，可能

2、存在矛盾、二義性、含糊性、 14.1.2 軟件開發(fā)過(guò)程中的數(shù) 學(xué) 數(shù)學(xué)最有用的性質(zhì)之一是，它能夠簡(jiǎn) 潔、準(zhǔn)確地描述物理現(xiàn)象、對(duì)象或動(dòng)作的 結(jié)果，因此是 理想的建模工具。 在軟件開發(fā)過(guò)程中使用數(shù)學(xué)的另一個(gè) 優(yōu)點(diǎn)是，可以在軟件工程活動(dòng)之間平滑地 過(guò)渡。不僅功能規(guī)格說(shuō)明，而且系統(tǒng)設(shè)計(jì) 也可以用數(shù)學(xué)表達(dá)，當(dāng)然，程序代碼也是 一種數(shù)學(xué)符號(hào) (雖然是一種相當(dāng)繁瑣、冗長(zhǎng) 的數(shù)學(xué)符號(hào) ) 數(shù)學(xué)作為軟件開發(fā)工具的最后一個(gè)優(yōu) 點(diǎn)是，它提供了高層確認(rèn)的手段?？梢允?用數(shù)學(xué)方法證明，設(shè)計(jì)符合規(guī)格說(shuō)明，程 序代碼正確地反映了設(shè)計(jì)結(jié)果。 14.1.3 應(yīng)用形式化方法的準(zhǔn) 則 為了

3、更好地發(fā)揮這種方法的長(zhǎng)處，下 面給出應(yīng)用形式化方法的幾條準(zhǔn)則，供讀 者在實(shí)際工作中使用。 選擇適用于當(dāng)前項(xiàng)目的符號(hào)系統(tǒng)。 應(yīng)該形式化，但不要過(guò)分形式化。 通常沒(méi)有必要對(duì)系統(tǒng)的每個(gè)方面都使用形 式化方法。 應(yīng)該進(jìn)行成本 / 不要放棄傳統(tǒng)的開發(fā)方法。把形式 化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒?起來(lái)是可能 的，而且由于取長(zhǎng)補(bǔ)短往往能 獲得很好的效果。 應(yīng)該建立詳盡的文檔。建議使用自 然語(yǔ)言注釋來(lái)配合形式化的規(guī)格說(shuō)明，以 不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。在系統(tǒng)開發(fā) 過(guò)程中必須一如既往地實(shí)施其他 SQA活動(dòng)。 不應(yīng)該盲目依賴形式化方法

4、，這種 應(yīng)該測(cè)試、測(cè)試再測(cè)試。由于形式 化方法不能保證系統(tǒng)絕對(duì)正確，因此，軟 應(yīng)該重用。即使使用了形式化方法， 軟件重用仍然是降低軟件成本和提高軟件 14.2 有窮狀態(tài)機(jī) 利用有窮狀態(tài)機(jī)可以準(zhǔn)確地描述一個(gè) 系統(tǒng)，因此是表達(dá)規(guī)格說(shuō)明的一種形式化 14.2.1 下面通過(guò)一個(gè)簡(jiǎn)單例子介紹有窮狀態(tài) 圖 14.1 保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換圖 表 14 . 1 當(dāng)前狀態(tài) 次態(tài) 轉(zhuǎn)盤動(dòng)作 保險(xiǎn)箱鎖定 A B 1L A 報(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)警

5、 從上面這個(gè)簡(jiǎn)單例子可以看出，一個(gè) 有窮狀態(tài)機(jī)包括下述 5個(gè)部分：狀態(tài)集 J、 輸入 集 K、由當(dāng)前狀態(tài)和當(dāng)前輸入確定下 一個(gè)狀態(tài) (次態(tài) )的轉(zhuǎn)換函數(shù) T、初始態(tài) S和 終態(tài)集 F。 如果使用更形式化的術(shù)語(yǔ)，一個(gè)有窮 狀態(tài)機(jī)可以表示為一個(gè) 5元組 (J， R， T， S， F)，其中： J K T是一個(gè)從 (J-F) K到 J的轉(zhuǎn)換函數(shù)； SJ F J 當(dāng)前狀態(tài) 菜單 +事件 所選擇的項(xiàng) 下個(gè)狀態(tài)為了對(duì)一個(gè)系統(tǒng)進(jìn)行規(guī)格說(shuō)明， 通常都需要對(duì)有窮狀態(tài)機(jī)做一個(gè)很有用的 擴(kuò)展，即在前述的 5元組中加入第 6個(gè)組 件 謂詞集 P，即

6、把有窮狀態(tài)機(jī)擴(kuò)展為一 個(gè) 6元組，其中每個(gè)謂詞都是系統(tǒng)全局狀態(tài) Y的函數(shù)。 轉(zhuǎn)換函數(shù) T現(xiàn)在是一個(gè)從 (J-F) K P 到 J 當(dāng)前狀態(tài) 菜單 +事件 所選擇的項(xiàng) + 14.2.2 為了說(shuō)明在實(shí)際工作中怎樣使用形式 化的方法，現(xiàn)在我們用有窮狀態(tài)機(jī)技術(shù)給 出電梯問(wèn)題的 規(guī)格說(shuō)明。 電梯按鈕的狀態(tài)轉(zhuǎn)換圖如圖 14.2所示。 令 EB(e,f)表示按下電梯 e內(nèi)的按鈕并請(qǐng)求 到 f層去。 EB(e,f)有兩個(gè)狀態(tài)，分別是按 鈕發(fā)光 (打開 )和不發(fā)光 (關(guān)閉 )。 EBON(e,f)：電梯按鈕 (e， f) EBOFF(e,f)：電梯按鈕 (e，

7、f) 如果電梯按鈕 (e,f)發(fā)光且電梯到達(dá) f 層，該按鈕將熄滅。相反如果按鈕熄滅， 則按下它時(shí)，按鈕將發(fā)光。上述描述中包 圖 14.2 電梯按鈕的狀態(tài)轉(zhuǎn) 換圖 EBP(e,f)：電梯按鈕 (e,f) EAF(e,f)：電梯 e到達(dá) f 為了定義與這些事件和狀態(tài)相聯(lián)系的 狀態(tài)轉(zhuǎn)換規(guī)則，需要一個(gè)謂詞 V， (e,f)， V(e,f)：電梯 e停在 f 接下來(lái)讓我們考慮樓層按鈕。令 FB(d,f)表示 f層的按鈕請(qǐng)求電梯向 d方向運(yùn) 動(dòng)，樓層按鈕 FB(d,f)的狀態(tài)轉(zhuǎn)換圖如圖 14.3 FBON(d,f)：樓層按鈕

8、 (d,f)打開； FBOFF(d,f)：樓層按鈕 (d,f)關(guān)閉。 如果樓層按鈕已經(jīng)打開，而且一部電 梯到達(dá) f層，則按鈕關(guān)閉。反之，如果樓層 按鈕原來(lái)是關(guān)閉的，被按下后該按鈕將打 FBP(d,f)：樓層按鈕 (d,f) EAF(1n,f)：電梯 1或 或 n到達(dá) f層 其中 1n表示或?yàn)?1或?yàn)?2或?yàn)?n 圖 14.3 樓層按鈕的狀態(tài)轉(zhuǎn) 換圖 為了定義與這些事件和狀態(tài)相聯(lián)系的 狀態(tài)轉(zhuǎn)換規(guī)則，同樣也需要一個(gè)謂詞，它 是 S(d,e， f) S(d,e,f)：電梯 e停在 f層并且移動(dòng)方 向由 d確定為向上 (d=U)或向下 (d

9、=D)或待定 (d=N) 這個(gè)謂詞實(shí)際上是一個(gè)狀態(tài)，形式化 使用謂詞 S(d,e,f)，形式化轉(zhuǎn)換規(guī)則 FBOFF(d,f)+FBP(d,f)+not S(d,1n,f) JX*9FBON(d,f) FBON(d,f)+EAF(1n,f)+S(d,1n,f) JX*9FBOFF(d,f) 其中， d=UorD 也就是說(shuō)，如果在 f層請(qǐng)求電梯向 d方 向運(yùn)動(dòng)的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該 按鈕被按下，并且當(dāng)時(shí)沒(méi)有正停在 f層準(zhǔn)備 向 d方向移動(dòng)的電梯，則該樓層按鈕打開。 反之，如果樓層按鈕已經(jīng)打開，且至少有 一部電梯到達(dá) f層，該部

10、電梯將朝 d方向運(yùn) 在討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時(shí)定義 的謂詞 V(e,f)，可以用謂詞 S(d,e,f)重新 V(e,f)=S(U， e,f)or S(D,e,f)or S(N,e,f) 定義電梯按鈕和樓層按鈕的狀態(tài)都很 簡(jiǎn)單、直觀的事情?，F(xiàn)在轉(zhuǎn)向討論電梯的 狀態(tài)及其轉(zhuǎn)換規(guī)則，就會(huì)出現(xiàn)一些復(fù)雜的 情況。一個(gè)電梯狀態(tài)實(shí)質(zhì)上包含許多子狀 態(tài) (例如，電梯減速、停止、開門、在一段 時(shí)間后自動(dòng)關(guān)門 ) M(d,e,f)：電梯 e正沿 d方向移動(dòng)，即 將到達(dá)的是第 f S(d,e,f)：電梯 e停在 f層，將朝 d方向 移動(dòng) (

11、尚未關(guān)門 ) W(e,f)：電梯 e在 f層等待 (已關(guān)門 )。 其中 S(d,e,f)狀態(tài)已在討論樓層按鈕時(shí) 定義過(guò)，但是，現(xiàn)在的定義更完備一些。 圖 14.4是電梯的狀態(tài)轉(zhuǎn)換圖。注意， 三個(gè)電梯停止?fàn)顟B(tài) S(U,e,f)、 S(N， e,f)和 S(D， e,f)已被組合成一個(gè)大的狀態(tài)，這樣 做的目的是減少狀態(tài)總數(shù)以簡(jiǎn)化流圖。 圖 14.4 電梯的狀態(tài)轉(zhuǎn)換圖 圖 14.4中包含了下述三個(gè)可觸發(fā)狀態(tài) 發(fā)生改變的事件 DC(e,f)：電梯 e在樓層 f ST(e,f)：電梯 e靠近 f層時(shí)觸發(fā)傳感器， 電梯控制

12、器決定在當(dāng)前樓層電梯是否停下。 RL：電梯按鈕或樓層按鈕被按下進(jìn)入 最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為 簡(jiǎn)單起見，這里給出的規(guī)則僅發(fā)生在關(guān)門 S(U， e,f)+DC(e,f) JX*9M(U， e,f+1) S(D， e,f)+DC(e,f) JX*9M(D,e,f-1) S(N,e,f)+DC(e,f) JX*9W(e,f) e停在 f 層準(zhǔn)備向上移動(dòng)，且門已經(jīng)關(guān)閉，則電 梯將向上一樓層移動(dòng)。第二條和第三條規(guī) 則，分別對(duì)應(yīng)于電梯即將下降或者沒(méi)有待 處理的請(qǐng)求的情況。 14.2.3 有窮狀態(tài)機(jī)方法采用了一種簡(jiǎn)單的格 當(dāng)前

13、狀態(tài) +事件 + JX*9下個(gè)狀態(tài) 這種形式的規(guī)格說(shuō)明易于書寫、易于 驗(yàn)證，而且可以比較容易地把它轉(zhuǎn)變成設(shè) 計(jì)或程序代碼。事實(shí)上，可以開發(fā)一個(gè) CASE工具把一個(gè)有窮狀態(tài)機(jī)規(guī)格說(shuō)明直接 轉(zhuǎn)變?yōu)樵创a。 維護(hù)可以通過(guò)重新轉(zhuǎn)變來(lái)實(shí)現(xiàn)，也就 是說(shuō)，如果需要一個(gè)新的狀態(tài)或事件，首 先修改規(guī)格說(shuō)明，然后直接由新的規(guī)格說(shuō) 有窮狀態(tài)機(jī)方法比數(shù)據(jù)流圖技術(shù)更精 確，而且和它一樣易于理解。不過(guò)，它也 有缺點(diǎn)：在開發(fā)一個(gè)大系統(tǒng)時(shí)三元組 (即狀 態(tài)、事件、謂詞 )的數(shù)量會(huì)迅速增長(zhǎng)。此外， 和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài) 機(jī)方法也沒(méi)有處理定時(shí)需求。下節(jié)將介紹 的 Petri網(wǎng)技術(shù)，是一種可處

14、理定時(shí)問(wèn)題的 14.3 Petri網(wǎng) 14.3.1 Petri網(wǎng)包含 4種元素：一組位置 P、一 組轉(zhuǎn)換 T、輸入函數(shù) I以及輸出函數(shù) O。圖 14.5舉例說(shuō)明了 Petri網(wǎng)的組成。 一組位置 P為 P1， P2， P3， P4，在 一組轉(zhuǎn)換 T為 t1， t2，在圖中用 圖 14.5 Petri網(wǎng)的組成 兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)，用由位置 I(t1)= P2,P4 I(t2)= P2 兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換 O(t1)= P1 O(t2)= P3， P3 注意，輸出函數(shù) O(t2)中有

15、兩個(gè) P3，是因?yàn)?有兩個(gè)箭頭由 t2指向 P3 更形式化的 Petri網(wǎng)結(jié)構(gòu)，是一個(gè)四元 組 C=(P,T,I,O) P= P1， ,Pn是一個(gè)有窮位置集， n0 T= t1,,tm是一個(gè)有窮轉(zhuǎn)換集， m0 ，且 T和 P I： TP 為輸入函數(shù)，是由轉(zhuǎn)換到位 置無(wú)序單位組 (bags) O： TP 為輸出函數(shù)，是由轉(zhuǎn)換到位 一個(gè)無(wú)序單位組或多重組是允許一個(gè) Petri網(wǎng)的標(biāo)記是在 Petri網(wǎng)中令牌 (token)的分配。例如，在圖 14.6中有 4個(gè) 令牌，其中一個(gè)在 P1中，兩個(gè)在 P2中， P3中 沒(méi)有，還有一

16、個(gè)在 P4中。上述標(biāo)記可以用 向量 (1， 2， 0， 1)表示。由于 P2和 P4中有 令牌，因此 t1啟動(dòng) (即被激發(fā) )。 通常，當(dāng)每個(gè)輸入位置所擁有的令牌 數(shù)等于從該位置到轉(zhuǎn)換的線數(shù)時(shí)，就允許 轉(zhuǎn)換。當(dāng) t1被激發(fā)時(shí)， P2和 P4上各有一個(gè)令 牌被移出，而 P1上則增加一個(gè)令牌。 Petri網(wǎng)中令牌總數(shù)不 是固定的，在這 個(gè)例子中兩個(gè)令牌被移出，而 P1上只能增 加一個(gè)令牌。 在圖 14.6中 P2上有令牌，因此 t2也可 以被激發(fā)。當(dāng) t2被激發(fā)時(shí)， P2上將移走一 個(gè)令牌，而 P3上新增加兩個(gè)令牌。 Petri網(wǎng) 具有非確定性，也就是說(shuō)，如果數(shù)個(gè)轉(zhuǎn)換 都達(dá)到了

17、激發(fā)條件，則其中任意一個(gè)都可 以被激發(fā)。 圖 14.6所示 Petri網(wǎng)的標(biāo)記為 (1， 2， 0， 1)， t1和 t2都可以被激發(fā)。假設(shè) t1被激發(fā)了， 則結(jié)果如圖 14.7所示，標(biāo)記為 (2， 1， 0， 0)。 此時(shí)，只有 t2可以被激發(fā)。如果 t2也 被激發(fā)了，則令牌從 P2中移出，兩個(gè)新令 牌被放在 P3上，結(jié)果如圖 14.8所示，標(biāo)記 為 (2， 0， 2， 0)。 圖 14.6 帶標(biāo)記的 Petri網(wǎng) 圖 14.7 圖 14.6的 Petri網(wǎng)在轉(zhuǎn)換 t1被激發(fā)后的情況 圖 14.8 圖 14.7的 Petri網(wǎng)在轉(zhuǎn)換 t2被激發(fā)后的情況 更形式

18、化地說(shuō)， Petri網(wǎng) C=(P,T,I,O)中 的標(biāo)記 M，是由一組位置 P到一組非負(fù)整數(shù) M： P 0， 1， 2， 這樣，帶有標(biāo)記的 Petri網(wǎng)成為一個(gè)五 元組 (P， T， I， O， M)。 對(duì) Petri網(wǎng)的一個(gè)重要擴(kuò)充是加入禁止 線。如圖 14.9所示，禁止線是用一個(gè)小圓 圈而不是用箭頭標(biāo)記的輸入線。 通常，當(dāng)每個(gè)輸入線上至少有一個(gè)令 牌，而禁止線上沒(méi)有令牌的時(shí)候，相應(yīng)的 轉(zhuǎn)換才是允許的。在圖 14.9中， P3上有一 個(gè)令牌而 P2上沒(méi)有令牌，因此轉(zhuǎn)換 t1可以被 激發(fā)。 圖 14.9 含禁止線的 Petri

19、網(wǎng) 14.3.2 讓我們把 Petri網(wǎng)應(yīng)用于上一節(jié)討論過(guò) 的電梯問(wèn)題。當(dāng)用 Petri網(wǎng)表示電梯系統(tǒng)的 規(guī)格說(shuō)明時(shí)，每個(gè)樓層用一個(gè)位置 Ff代表 (1fm) ，在 Petri網(wǎng)中電梯是用一個(gè)令 牌代表的。在位置 Ff上有令牌，表示在樓 層 f 1. 為了用 Petri網(wǎng)表達(dá)電梯按鈕的規(guī)格說(shuō) 明，在 Petri網(wǎng)中還必須設(shè)置其他的位置。 電梯中樓層 f的按鈕，在 Petri網(wǎng)中用位置 EBf表示 (1fm) 。在 EBf上有一個(gè)令牌， 就表示電梯內(nèi)樓層 f 電梯按鈕只有在第一次被按下時(shí)才會(huì) 由暗變亮，以后再按它則只會(huì)被忽略。圖 14.10所示的 Petri網(wǎng)

20、準(zhǔn)確地描述了電梯按 鈕的行為規(guī)律。首先，假設(shè)按鈕沒(méi)有發(fā)亮， 顯然在位置 EBf上沒(méi)有令牌，從而在存在禁 止線的情況下，轉(zhuǎn)換 “ EBf被按下 ” 是允許 發(fā)生的。 假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)換被激發(fā)并 在 EBf上放置了一個(gè)令牌，如圖 14.10所示。 以后不論再按下多少次按鈕，禁止線與現(xiàn) 有令牌的組合都決定了轉(zhuǎn)換 “ EBf被按下 ” 不能再被激發(fā)了，因此，位置 EBf上的令牌 數(shù)不會(huì)多于 1 圖 14.10 Petri網(wǎng)表示的電梯按鈕 假設(shè)電梯由 g層駛向 f層，因?yàn)殡娞菰?g 層，如圖 14.10所示，位置 Fg上有一個(gè)令牌。 由于每條輸入線上各有一個(gè)令牌，轉(zhuǎn)換 “ 電梯在運(yùn)

21、行 ” 被激發(fā)，從而 EBf和 Fg上的 令牌被移走，按鈕 EBf被關(guān)閉，在位置 Ff上 出現(xiàn)一個(gè)新令牌，即轉(zhuǎn)換的激發(fā)使電梯由 g 層駛到 f 事實(shí)上，電梯由 g層移到 f層是需要時(shí) 間的，為處理這個(gè)情況及其他類似的問(wèn)題 (例如，由于物理上的原因按鈕被按下后不 能馬上發(fā)亮 )， Petri網(wǎng)模型中必須加入時(shí) 限。 也就是說(shuō)，在標(biāo)準(zhǔn) Petri網(wǎng)中轉(zhuǎn)換是瞬 時(shí)完成的，而在現(xiàn)實(shí)情況下就需要時(shí)間控 制 Petri網(wǎng)，以使轉(zhuǎn)換與非零時(shí)間相聯(lián)系。 2. 樓層按鈕 在 Petri網(wǎng)中樓層按鈕用位置 和 表示，分別代表 f樓層請(qǐng)求電梯上行和下行 的按鈕。底層的按鈕為

22、 ，最高層的按 鈕為 ，中間每一層有兩個(gè)按鈕 和 (1 f m) ufFB dfFB uFB1 dmFB ufFB dfFB 圖 14.11 Petri網(wǎng)表示樓層按鈕 第三條約束 C3：當(dāng)電梯沒(méi)有收到請(qǐng)求 這條約束很容易實(shí)現(xiàn)，如圖 14.11所 示，當(dāng)沒(méi)有請(qǐng)求 ( 和 上無(wú)令牌 )時(shí)， 任何一個(gè)轉(zhuǎn)換“電梯在運(yùn)行”都不能被激 發(fā)。 ufFB d fFB 14.4 Z語(yǔ)言 14.4.1 簡(jiǎn)介 本節(jié)結(jié)合電梯問(wèn)題的例子，簡(jiǎn)要地介紹 Z 用 Z語(yǔ)言描述的、最簡(jiǎn)單的形式化規(guī)格 說(shuō)明含有下述 4

23、 現(xiàn)在依次介紹這 4 1. 一個(gè) Z規(guī)格說(shuō)明從一系列給定的初始化 集合開始。所謂初始化集合就是不需要詳 細(xì)定義的集合，這種集合用帶方括號(hào)的形 式表示。對(duì)于電梯問(wèn)題，給定的初始化集 合稱為 Button，即所有按鈕的集合，因此， Z Button 2. 一個(gè) Z規(guī)格說(shuō)明由若干個(gè) “ 格 (schema)” 組成，每個(gè)格含有一組變量說(shuō)明和一系列 限定變量取值范圍的謂詞。例如，格 S的格 式如圖 14.12 在電梯問(wèn)題中， Button有 4個(gè)子集，即 floor_buttons(樓層按鈕的集合 )、 elevator_buttons(

24、電梯按鈕的集合 )、 buttons(電梯問(wèn)題中所有按鈕的集合 )以及 pushed(所有被按的按鈕的集合，即所有處 于打開狀態(tài)的按鈕的集合 )。圖 14.13描述 了格 Button_State，其中，符號(hào) P表示冪集 (即給定集的所有子集 )。 約束條件聲明， floor_buttons集與 elevator_buttons集不相交，而且它們共 同組成 buttons集 (在下面的討論中并不需 要 floor_buttons集和 elevator_buttons集， 把它們放于圖 14.13中只是用來(lái)說(shuō)明 Z格包 含的內(nèi)容 ) 圖 14.12 Z格 S的格式 圖 14.13

25、Z格 Button_State 3. 抽象的初始狀態(tài)是指系統(tǒng)第一次開啟 時(shí)的狀態(tài)。對(duì)于電梯問(wèn)題來(lái)說(shuō)，抽象的初 Button_Init Button_State pushed= 上式表示，當(dāng)系統(tǒng)首次開啟時(shí) pushed 4. 如果一個(gè)原來(lái)處于關(guān)閉狀態(tài)的按鈕被 按下，則該按鈕開啟，這個(gè)按鈕就被添加 到 pushed集中。圖 14.14定義了操作 Push_Button(按按鈕 )。 Z語(yǔ)言的語(yǔ)法規(guī)定，當(dāng)一個(gè)格被用在另 一個(gè)格中時(shí)，要在它的前面加上三角形符 號(hào)作為前綴，因此，格 Push_Button的第 一行最前面有一個(gè)三角形符號(hào)作為格 Button

26、_State的前綴。 操作 Push_Button有一個(gè)輸入變量 “ button?”。問(wèn)號(hào) “ ?”表示輸入變量，而 感嘆號(hào) “ !”代表輸出變量。 操作的謂詞部分，包含了一組調(diào)用操 作的前置條件，以及操作完全結(jié)束后的后 置條件。如果前置條件成立，則操作執(zhí)行 完成后可得到后置條件。但是，如果在前 置條件不成立的情況下調(diào)用該操作，則不 能得到指定的結(jié)果 (因此結(jié)果無(wú)法預(yù)測(cè) )。 圖 14.14中的第一個(gè)前置條件規(guī)定， “ button?”必須是 buttons的一個(gè)元素， 而 buttons是電梯系統(tǒng)中所有按鈕的集合。 如果第二個(gè)前置條件 button? pushed得到

27、 滿足 (即按鈕沒(méi)有開啟 )，則更新 pushed按 鈕集，使之包含剛開啟的按鈕 “ button?”。 在 Z語(yǔ)言中，當(dāng)一個(gè)變量的值發(fā)生改變 時(shí)，就用符號(hào) “” 表示。也就是說(shuō)，后 置條件是當(dāng)執(zhí)行完操作 Push_Button之后， “ button?”將被加入到 pushed集中。我們 無(wú)需直接打開按鈕，只要使 “ button?”變 成 pushed 圖 14.14 操作 Push_Button的 Z規(guī)格說(shuō)明 還有一種可能性是，被按的按鈕原先 已經(jīng)打開了。由于 button?pushed ，根據(jù) 第三個(gè)前置條件，將沒(méi)有任何事情發(fā)生， 這可以用 pushed=pushed

28、 來(lái)表示，即 pushed的新狀態(tài)和舊狀態(tài)一樣。 注意，如果沒(méi)有第三個(gè)前置條件，規(guī) 格說(shuō)明將不能說(shuō)明在一個(gè)按鈕已被按過(guò)之 后又被按了一次的情況下將發(fā)生什么事， 假設(shè)電梯到達(dá)了某樓層，如果相應(yīng)的 樓層按鈕已經(jīng)打開，則此時(shí)它會(huì)關(guān)閉；同 樣，如果相應(yīng)的電梯按鈕已經(jīng)打開，則此 時(shí)它也會(huì)關(guān)閉。也就是說(shuō)，如果 “ button?” 屬于 pushed集，則將它移出該集合，如圖 14.15所示 (符號(hào) “ ” 表示集合差運(yùn)算 )。 但是，如果按鈕 “ button?”原先沒(méi)有 打開，則 pushed集合不發(fā)生變化。 本節(jié)的討論有所簡(jiǎn)化，沒(méi)有區(qū)分上行 和下行樓層按鈕，但是，仍然講清

29、了使用 Z 圖 14.15 操作 Floor_Arrival的 Z規(guī)格說(shuō)明 14.4.2 已經(jīng)在許多軟件開發(fā)項(xiàng)目中成功地運(yùn) 用了 Z語(yǔ)言，目前， Z也許是應(yīng)用得最廣泛 的形式化語(yǔ)言，尤其是在大型項(xiàng)目中 Z語(yǔ)言 的優(yōu)勢(shì)更加明顯。 Z語(yǔ)言之所以會(huì)獲得如此 可以比較容易地發(fā)現(xiàn)用 Z寫的規(guī)格 說(shuō)明的錯(cuò)誤，特別是在自己審查規(guī)格說(shuō)明， 及根據(jù)形式化的規(guī)格說(shuō)明來(lái)審查設(shè)計(jì)與代 用 Z寫規(guī)格說(shuō)明時(shí)，要求作者十分 精確地使用 Z說(shuō)明符。由于對(duì)精確性的要求 很高，從而和非形式化規(guī)格說(shuō)明相比，減 Z 是一種形式化語(yǔ)言，在需要時(shí)開 發(fā)者可以嚴(yán)格地驗(yàn)證規(guī)格說(shuō)明的正確

30、性。 雖然完全學(xué)會(huì) Z語(yǔ)言相當(dāng)困難，但 是，經(jīng)驗(yàn)表明，只學(xué)過(guò)中學(xué)數(shù)學(xué)的軟件開 發(fā)人員仍然可以只用比較短的時(shí)間就學(xué)會(huì) 編寫 Z規(guī)格說(shuō)明，當(dāng)然，這些人還沒(méi)有能力 使用 Z語(yǔ)言可以降低軟件開發(fā)費(fèi)用。 雖然用 Z寫規(guī)格說(shuō)明所需用的時(shí)間比使用非 形式化技術(shù)要多，但開發(fā)過(guò)程所需要的總 雖然用戶無(wú)法理解用 Z寫的規(guī)格說(shuō) 明，但是，可以依據(jù) Z規(guī)格說(shuō)明用自然語(yǔ)言 重寫規(guī)格說(shuō)明。經(jīng)驗(yàn)證明，這樣得到的自 然語(yǔ)言規(guī)格說(shuō)明，比直接用自然語(yǔ)言寫出 使用形式化規(guī)格說(shuō)明是全球的總趨勢(shì)， 過(guò)去，主要是歐洲習(xí)慣于使用形式化規(guī)格 說(shuō)明技術(shù)，現(xiàn)在越來(lái)越多的美國(guó)公司也開

31、 14.5 小結(jié) 基于數(shù)學(xué)的形式化規(guī)格說(shuō)明技術(shù)，目 前還沒(méi)有在軟件產(chǎn)業(yè)界廣泛應(yīng)用，但是， 與欠形式化的方法比較起來(lái)，它確實(shí)有實(shí) 質(zhì)性的優(yōu)點(diǎn)： 形式化的規(guī)格說(shuō)明可以用數(shù)學(xué)方法研 究、驗(yàn)證 (例如，一個(gè)正確的程序可以被證 明滿足其規(guī)格說(shuō)明，兩個(gè)規(guī)格說(shuō)明可以被 證明是等價(jià)的，規(guī)格說(shuō)明中存在的某些形 式的不完整性和不一致性可以被自動(dòng)地檢 測(cè)出來(lái) )。 此外，形式化的規(guī)格說(shuō)明消除了二義 性，而且它鼓勵(lì)軟件開發(fā)者在軟件工程過(guò) 程的早期階段使用更嚴(yán)格的方法，從而可 當(dāng)然，形式化方法也有缺點(diǎn)：大多數(shù) 形式化的規(guī)格說(shuō)明主要關(guān)注于系統(tǒng)的功能 和數(shù)據(jù)，而問(wèn)題的時(shí)序、控制和行為等方 面的需求卻更難于表示。此外，形式化方 法比欠形式化方法更難學(xué)習(xí)，不僅在培訓(xùn) 階段要花大量的投資，而且對(duì)某些軟件工 程師來(lái)說(shuō)，它代表了一種 “ 文化沖擊 ” 。 把形式化方法和欠形式化方法有機(jī)地 結(jié)合起來(lái)，使它們?nèi)￠L(zhǎng)補(bǔ)短，應(yīng)該能獲得 更理想的效果。本章講述的應(yīng)用形式化方 法的準(zhǔn)則 (見 14.1.3節(jié) )，對(duì)于讀者今后在 實(shí)際工作中更好地利用形式化方法，可能 本章簡(jiǎn)要地介紹了有窮狀態(tài)機(jī)、 Petri 網(wǎng)和 Z語(yǔ)言等三種典型的形式化方法，使讀 者對(duì)它們有初步的、概括的了解。當(dāng)然， 要想在實(shí)際工作中使用這些方法，還需要