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

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

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

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

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

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

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

7、f) 如果電梯按鈕 (e,f)發(fā)光且電梯到達(dá) f 層，該按鈕將熄滅。相反如果按鈕熄滅， 則按下它時，按鈕將發(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ī)則，需要一個謂詞 V， (e,f)， V(e,f)：電梯 e停在 f 接下來讓我們考慮樓層按鈕。令 FB(d,f)表示 f層的按鈕請求電梯向 d方向運 動，樓層按鈕 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)閉。反之，如果樓層 按鈕原來是關(guān)閉的，被按下后該按鈕將打 FBP(d,f)：樓層按鈕 (d,f) EAF(1n,f)：電梯 1或 或 n到達(dá) f層 其中 1n表示或為 1或為 2或為 n 圖 14.3 樓層按鈕的狀態(tài)轉(zhuǎn) 換圖 為了定義與這些事件和狀態(tài)相聯(lián)系的 狀態(tài)轉(zhuǎn)換規(guī)則，同樣也需要一個謂詞，它 是 S(d,e， f) S(d,e,f)：電梯 e停在 f層并且移動方 向由 d確定為向上 (d=U)或向下 (d

9、=D)或待定 (d=N) 這個謂詞實際上是一個狀態(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 也就是說，如果在 f層請求電梯向 d方 向運動的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該 按鈕被按下，并且當(dāng)時沒有正停在 f層準(zhǔn)備 向 d方向移動的電梯，則該樓層按鈕打開。 反之，如果樓層按鈕已經(jīng)打開，且至少有 一部電梯到達(dá) f層，該部

10、電梯將朝 d方向運 在討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時定義 的謂詞 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)都很 簡單、直觀的事情?，F(xiàn)在轉(zhuǎn)向討論電梯的 狀態(tài)及其轉(zhuǎn)換規(guī)則，就會出現(xiàn)一些復(fù)雜的 情況。一個電梯狀態(tài)實質(zhì)上包含許多子狀 態(tài) (例如，電梯減速、停止、開門、在一段 時間后自動關(guān)門 ) M(d,e,f)：電梯 e正沿 d方向移動，即 將到達(dá)的是第 f S(d,e,f)：電梯 e停在 f層，將朝 d方向 移動 (

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

12、器決定在當(dāng)前樓層電梯是否停下。 RL：電梯按鈕或樓層按鈕被按下進(jìn)入 最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為 簡單起見，這里給出的規(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)備向上移動，且門已經(jīng)關(guān)閉，則電 梯將向上一樓層移動。第二條和第三條規(guī) 則，分別對應(yīng)于電梯即將下降或者沒有待 處理的請求的情況。 14.2.3 有窮狀態(tài)機方法采用了一種簡單的格 當(dāng)前

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

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

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

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

17、激發(fā)條件，則其中任意一個都可 以被激發(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)。 此時，只有 t2可以被激發(fā)。如果 t2也 被激發(fā)了，則令牌從 P2中移出，兩個新令 牌被放在 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、化地說， Petri網(wǎng) C=(P,T,I,O)中 的標(biāo)記 M，是由一組位置 P到一組非負(fù)整數(shù) M： P 0， 1， 2， 這樣，帶有標(biāo)記的 Petri網(wǎng)成為一個五 元組 (P， T， I， O， M)。 對 Petri網(wǎng)的一個重要擴(kuò)充是加入禁止 線。如圖 14.9所示，禁止線是用一個小圓 圈而不是用箭頭標(biāo)記的輸入線。 通常，當(dāng)每個輸入線上至少有一個令 牌，而禁止線上沒有令牌的時候，相應(yīng)的 轉(zhuǎn)換才是允許的。在圖 14.9中， P3上有一 個令牌而 P2上沒有令牌，因此轉(zhuǎn)換 t1可以被 激發(fā)。 圖 14.9 含禁止線的 Petri

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

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

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

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

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

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

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

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

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

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

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

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

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