軟件工程課件之第4章_形式化說明技術(shù)(第五版)(張海潘編著)

1、4.1 概述概述4.2 有窮狀態(tài)機(jī)有窮狀態(tài)機(jī)4.3 Petri網(wǎng)網(wǎng)4.4 Z語言語言第第4章章 形式化說明技術(shù)形式化說明技術(shù)軟件工程使用方法的分類：軟件工程使用方法的分類：n非形式化，用自然語言描述需求規(guī)格說明；非形式化，用自然語言描述需求規(guī)格說明；n半形式化，用數(shù)據(jù)流圖或?qū)嶓w半形式化，用數(shù)據(jù)流圖或?qū)嶓w-聯(lián)系圖建立模聯(lián)系圖建立模型；型；n形式化，是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)，形式化，是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)，也就是說，如果一種方法有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)，也就是說，如果一種方法有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的。那么它就是形式化的。 4.1 概述概述4.1.1 非形式化方法的缺點(diǎn)非形式化方法

2、的缺點(diǎn)n矛盾，指一組相互沖突的陳述。矛盾，指一組相互沖突的陳述。n二義性，指讀者可以用不同方式理解的陳述。二義性，指讀者可以用不同方式理解的陳述。n含糊性，幾乎不可避免地會(huì)出現(xiàn)含糊性。含糊性，幾乎不可避免地會(huì)出現(xiàn)含糊性。n不完整性，不完整性可能是在系統(tǒng)規(guī)格說明不完整性，不完整性可能是在系統(tǒng)規(guī)格說明中最常遇到的問題之一。中最常遇到的問題之一。n抽象層次混亂，指在非常抽象的陳述中混進(jìn)抽象層次混亂，指在非常抽象的陳述中混進(jìn)了一些關(guān)于細(xì)節(jié)的低層次陳述。了一些關(guān)于細(xì)節(jié)的低層次陳述。 4.1.2 形式化方法的優(yōu)點(diǎn)形式化方法的優(yōu)點(diǎn)n數(shù)學(xué)能夠簡(jiǎn)潔準(zhǔn)確地描述物理現(xiàn)象、對(duì)象或動(dòng)數(shù)學(xué)能夠簡(jiǎn)潔準(zhǔn)確地描述物理現(xiàn)象、對(duì)象

3、或動(dòng)作的結(jié)果，因此是理想的建模工具。特別適合作的結(jié)果，因此是理想的建模工具。特別適合于表示狀態(tài)，也就是表示于表示狀態(tài)，也就是表示“做什么做什么”。n可以在不同的軟件工程活動(dòng)之間平滑地過渡。可以在不同的軟件工程活動(dòng)之間平滑地過渡。不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計(jì)也可以用數(shù)不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計(jì)也可以用數(shù)學(xué)表達(dá)，當(dāng)然，程序代碼也是一種數(shù)學(xué)符號(hào)。學(xué)表達(dá)，當(dāng)然，程序代碼也是一種數(shù)學(xué)符號(hào)。n它提供了高層確認(rèn)的手段?？梢允褂脭?shù)學(xué)方法它提供了高層確認(rèn)的手段。可以使用數(shù)學(xué)方法證明，設(shè)計(jì)符合規(guī)格說明，程序代碼正確地實(shí)證明，設(shè)計(jì)符合規(guī)格說明，程序代碼正確地實(shí)現(xiàn)了設(shè)計(jì)結(jié)果?，F(xiàn)了設(shè)計(jì)結(jié)果。 4.1.3 應(yīng)用形式

4、化方法的準(zhǔn)則應(yīng)用形式化方法的準(zhǔn)則(1) 應(yīng)該選用適當(dāng)?shù)谋硎痉椒☉?yīng)該選用適當(dāng)?shù)谋硎痉椒?通常，一種規(guī)格說明技術(shù)只能用自然的方通常，一種規(guī)格說明技術(shù)只能用自然的方式說明某一類概念。式說明某一類概念。(2) 應(yīng)該形式化，但不要過分形式化應(yīng)該形式化，但不要過分形式化 目前的形式化技術(shù)還不適于描述系統(tǒng)的每目前的形式化技術(shù)還不適于描述系統(tǒng)的每個(gè)方面。個(gè)方面。(3) 應(yīng)該估算成本應(yīng)該估算成本 為了使用形式化方法，通常需要事先進(jìn)行為了使用形式化方法，通常需要事先進(jìn)行大量的培訓(xùn)。最好預(yù)先估算所需的成本并編入大量的培訓(xùn)。最好預(yù)先估算所需的成本并編入預(yù)算。預(yù)算。(4) 應(yīng)該有形式化方法顧問隨時(shí)提供咨詢應(yīng)該有形式化方

5、法顧問隨時(shí)提供咨詢 絕大多數(shù)軟件工程師對(duì)形式化方法中使用絕大多數(shù)軟件工程師對(duì)形式化方法中使用的數(shù)學(xué)和邏輯并不很熟悉，沒受過使用形式化的數(shù)學(xué)和邏輯并不很熟悉，沒受過使用形式化方法的專業(yè)訓(xùn)練，因此需要專家指導(dǎo)和培訓(xùn)。方法的專業(yè)訓(xùn)練，因此需要專家指導(dǎo)和培訓(xùn)。(5) 不應(yīng)該放棄傳統(tǒng)的開發(fā)方法不應(yīng)該放棄傳統(tǒng)的開發(fā)方法 把形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓桨研问交椒ê徒Y(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋砣￠L(zhǎng)補(bǔ)短往往能獲得很好的效果。法集成起來取長(zhǎng)補(bǔ)短往往能獲得很好的效果。 (6) 應(yīng)該建立詳盡的文檔應(yīng)該建立詳盡的文檔 建議使用自然語言注釋形式化的規(guī)格說明建議使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和維

6、護(hù)人員理解系統(tǒng)。書，以幫助用戶和維護(hù)人員理解系統(tǒng)。 (7) 不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn) 形式化方法不能保證軟件的正確性，只不形式化方法不能保證軟件的正確性，只不過是有助于開發(fā)出高質(zhì)量軟件的一種手段。過是有助于開發(fā)出高質(zhì)量軟件的一種手段。 (8) 不應(yīng)該盲目依賴形式化方法不應(yīng)該盲目依賴形式化方法 形式化方法并不能保證開發(fā)出的軟件絕對(duì)形式化方法并不能保證開發(fā)出的軟件絕對(duì)正確，必須用其他方法來驗(yàn)證軟件正確性。正確，必須用其他方法來驗(yàn)證軟件正確性。(9) 應(yīng)該測(cè)試、測(cè)試再測(cè)試應(yīng)該測(cè)試、測(cè)試再測(cè)試 軟件測(cè)試的重要性并沒有降低。軟件測(cè)試的重要性并沒有降低。(10) 應(yīng)該重用應(yīng)該重用 軟件重用仍然

7、是降低軟件成本和提高軟件軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的惟一合理的方法。質(zhì)量的惟一合理的方法。4.2 有窮狀態(tài)機(jī)有窮狀態(tài)機(jī)4.2.1 概念概念 例：例： 一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)記為個(gè)位置，分別標(biāo)記為1、2、3，轉(zhuǎn)盤可向左，轉(zhuǎn)盤可向左(L)或向右或向右(R)轉(zhuǎn)動(dòng)。這樣，在任意時(shí)刻轉(zhuǎn)盤都有轉(zhuǎn)動(dòng)。這樣，在任意時(shí)刻轉(zhuǎn)盤都有6種可能的運(yùn)動(dòng)，即種可能的運(yùn)動(dòng)，即1L、1R、2L、2R、3L和和3R。保險(xiǎn)箱的組合密碼是。保險(xiǎn)箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤，轉(zhuǎn)盤的任何其他運(yùn)動(dòng)都將引起報(bào)警。的任何其他運(yùn)動(dòng)都將引起報(bào)警。 有窮狀態(tài)機(jī)包括有窮

8、狀態(tài)機(jī)包括5個(gè)部分：個(gè)部分：狀態(tài)集狀態(tài)集J、輸入集輸入集K、由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個(gè)狀態(tài)由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個(gè)狀態(tài)(次態(tài)次態(tài))的的轉(zhuǎn)換函數(shù)轉(zhuǎn)換函數(shù)T、初始態(tài)初始態(tài)S和和終態(tài)集終態(tài)集F。n狀態(tài)集狀態(tài)集J：保險(xiǎn)箱鎖定，：保險(xiǎn)箱鎖定，A，B，保險(xiǎn)箱解鎖，保險(xiǎn)箱解鎖，報(bào)警報(bào)警n輸入集輸入集K：1L，1R，2L，2R，3L，3Rn轉(zhuǎn)換函數(shù)轉(zhuǎn)換函數(shù)T：如表：如表4.1所示所示n初始態(tài)初始態(tài)S：保險(xiǎn)箱鎖定：保險(xiǎn)箱鎖定n終態(tài)集終態(tài)集F：保險(xiǎn)箱解鎖，報(bào)警：保險(xiǎn)箱解鎖，報(bào)警表表 4 4 . .1 1 保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換表保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換表當(dāng)前狀態(tài)當(dāng)前狀態(tài) 次態(tài)次態(tài)轉(zhuǎn)盤動(dòng)作轉(zhuǎn)盤動(dòng)作保險(xiǎn)箱鎖定保險(xiǎn)箱鎖定A

9、 AB B1L1LA A報(bào)警報(bào)警報(bào)警報(bào)警1R1R報(bào)警報(bào)警報(bào)警報(bào)警報(bào)警報(bào)警2L2L報(bào)警報(bào)警報(bào)警報(bào)警保險(xiǎn)箱解鎖保險(xiǎn)箱解鎖2R2R報(bào)警報(bào)警報(bào)警報(bào)警報(bào)警報(bào)警3L3L報(bào)警報(bào)警報(bào)警報(bào)警報(bào)警報(bào)警3R3R報(bào)警報(bào)警B B報(bào)警報(bào)警4.2.3 評(píng)價(jià)評(píng)價(jià)優(yōu)點(diǎn)：優(yōu)點(diǎn)：n形式簡(jiǎn)單，易于書寫、易于驗(yàn)證，比較容易地形式簡(jiǎn)單，易于書寫、易于驗(yàn)證，比較容易地把它轉(zhuǎn)變成設(shè)計(jì)或程序代碼。把它轉(zhuǎn)變成設(shè)計(jì)或程序代碼。n比數(shù)據(jù)流圖技術(shù)更精確，而且和它一樣易于理比數(shù)據(jù)流圖技術(shù)更精確，而且和它一樣易于理解。解。缺點(diǎn)：缺點(diǎn)：n在開發(fā)一個(gè)大系統(tǒng)時(shí)三元組在開發(fā)一個(gè)大系統(tǒng)時(shí)三元組(即狀態(tài)、事件、即狀態(tài)、事件、謂詞謂詞)的數(shù)量會(huì)迅速增長(zhǎng)。的數(shù)量會(huì)迅速增

10、長(zhǎng)。n和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機(jī)方和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機(jī)方法也沒有處理定時(shí)需求。法也沒有處理定時(shí)需求。 4.3 Petri網(wǎng)網(wǎng)4.3.1 概念概念 并發(fā)系統(tǒng)中遇到的一個(gè)主要問題是定時(shí)問并發(fā)系統(tǒng)中遇到的一個(gè)主要問題是定時(shí)問題。這個(gè)問題可以表現(xiàn)為多種形式，如同步問題。這個(gè)問題可以表現(xiàn)為多種形式，如同步問題、競(jìng)爭(zhēng)條件以及死鎖問題。如果規(guī)格說明不題、競(jìng)爭(zhēng)條件以及死鎖問題。如果規(guī)格說明不恰當(dāng)，則有導(dǎo)致不完善的設(shè)計(jì)或?qū)崿F(xiàn)的危險(xiǎn)。恰當(dāng)，則有導(dǎo)致不完善的設(shè)計(jì)或?qū)崿F(xiàn)的危險(xiǎn)。用于確定系統(tǒng)中隱含的定時(shí)問題的一種有效技用于確定系統(tǒng)中隱含的定時(shí)問題的一種有效技術(shù)是術(shù)是Petri網(wǎng)，這種技術(shù)的

11、一個(gè)很大的優(yōu)點(diǎn)是網(wǎng)，這種技術(shù)的一個(gè)很大的優(yōu)點(diǎn)是它也可以用于設(shè)計(jì)中。它也可以用于設(shè)計(jì)中。 Petri網(wǎng)結(jié)構(gòu)，是一個(gè)四元組網(wǎng)結(jié)構(gòu)，是一個(gè)四元組C=(P,T,I,O)。其中。其中nP=P1,Pn是一個(gè)有窮位置集，是一個(gè)有窮位置集，n0。nT=t1,tm是一個(gè)有窮轉(zhuǎn)換集，是一個(gè)有窮轉(zhuǎn)換集，m0，且，且T和和P不相交。不相交。nI：TP為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組位組(bags)的映射。的映射。nO：TP為輸出函數(shù)，是由轉(zhuǎn)換到位置無序?yàn)檩敵龊瘮?shù)，是由轉(zhuǎn)換到位置無序單位組的映射。單位組的映射。 n一組位置一組位置P為為P1，P2，P3，P4，用圓圈代表位置。，用圓圈

12、代表位置。n一組轉(zhuǎn)換一組轉(zhuǎn)換T為為t1，t2，用短直線表示轉(zhuǎn)換。，用短直線表示轉(zhuǎn)換。n兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是：表示，它們是：I(t1)=P2，P4，I(t2)=P2n兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是：表示，它們是：O(t1)=P1，O(t2)=P3，P3位置位置轉(zhuǎn)換轉(zhuǎn)換輸入輸入輸出輸出帶標(biāo)記的帶標(biāo)記的Petri網(wǎng)：網(wǎng)：通常，當(dāng)每個(gè)通常，當(dāng)每個(gè)輸入位置所擁有輸入位置所擁有的權(quán)標(biāo)數(shù)大于等的權(quán)標(biāo)數(shù)大于等于從該位置到轉(zhuǎn)于從該位置到轉(zhuǎn)換的線數(shù)時(shí)，就換的

13、線數(shù)時(shí)，就允許轉(zhuǎn)換。允許轉(zhuǎn)換。(1,2,0,1) (2,1,0,0) (2,0,2,0) 權(quán)標(biāo)數(shù)權(quán)標(biāo)數(shù)加入禁止線的加入禁止線的Petri網(wǎng)：網(wǎng)： 禁止線是用一個(gè)小圓圈而不是用箭頭標(biāo)記禁止線是用一個(gè)小圓圈而不是用箭頭標(biāo)記的輸入線。通常，當(dāng)每個(gè)輸入線上至少有一個(gè)的輸入線。通常，當(dāng)每個(gè)輸入線上至少有一個(gè)權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)的時(shí)候，相應(yīng)的轉(zhuǎn)權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)的時(shí)候，相應(yīng)的轉(zhuǎn)換才是允許的。換才是允許的。 禁止線禁止線輸入線輸入線4.4 Z語言語言4.4.1 簡(jiǎn)介簡(jiǎn)介 用用Z語言描述的、最簡(jiǎn)單的形式化規(guī)格說語言描述的、最簡(jiǎn)單的形式化規(guī)格說明含有下述明含有下述4個(gè)部分：個(gè)部分：n給定的集合、數(shù)據(jù)類

14、型及常數(shù)；給定的集合、數(shù)據(jù)類型及常數(shù)；n狀態(tài)定義；狀態(tài)定義；n初始狀態(tài)；初始狀態(tài)；n操作。操作。 1. 給定的集合給定的集合 一個(gè)一個(gè)Z規(guī)格說明從一系列給定的初始化集規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細(xì)定義合開始。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集合用帶方括號(hào)的形式表示。對(duì)的集合，這種集合用帶方括號(hào)的形式表示。對(duì)于電梯問題，給定的初始化集合稱為于電梯問題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，即所有按鈕的集合，因此，Z規(guī)格說明開始于：規(guī)格說明開始于：Button 2. 狀態(tài)定義狀態(tài)定義 一個(gè)一個(gè)Z規(guī)格說明由若干個(gè)規(guī)格說明由若干個(gè)“格

15、格(schema)”組成，每個(gè)格含有一組變量說明和一系列限定組成，每個(gè)格含有一組變量說明和一系列限定變量取值范圍的謂詞。變量取值范圍的謂詞。3. 初始狀態(tài)初始狀態(tài) 抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時(shí)的抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時(shí)的狀態(tài)。對(duì)于電梯問題來說，抽象的初始狀態(tài)為：狀態(tài)。對(duì)于電梯問題來說，抽象的初始狀態(tài)為： Button_Init Button_Statepushed= 上式表示，當(dāng)系統(tǒng)首次開啟時(shí)上式表示，當(dāng)系統(tǒng)首次開啟時(shí)pushed集集為空，即所有按鈕都處于關(guān)閉狀態(tài)。為空，即所有按鈕都處于關(guān)閉狀態(tài)。4. 操作操作 如果一個(gè)原來處于關(guān)閉狀態(tài)的按鈕被按下，如果一個(gè)原來處于關(guān)閉狀態(tài)的按

16、鈕被按下，則該按鈕開啟，這個(gè)按鈕就被添加到則該按鈕開啟，這個(gè)按鈕就被添加到pushed集中。集中。4.4.2 評(píng)價(jià)評(píng)價(jià)(1) 可以比較容易地發(fā)現(xiàn)用可以比較容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯(cuò)誤。寫的規(guī)格說明的錯(cuò)誤。(2) 用用Z寫規(guī)格說明時(shí)，要求作者十分精確地使用寫規(guī)格說明時(shí)，要求作者十分精確地使用Z說明說明符，減少了模糊性、不一致性和遺漏。符，減少了模糊性、不一致性和遺漏。(3) Z是一種形式化語言，在需要時(shí)開發(fā)者可以嚴(yán)格地驗(yàn)是一種形式化語言，在需要時(shí)開發(fā)者可以嚴(yán)格地驗(yàn)證規(guī)格說明的正確性。證規(guī)格說明的正確性。(4) 雖然完全學(xué)會(huì)雖然完全學(xué)會(huì)Z語言相當(dāng)困難，但是，經(jīng)驗(yàn)表明，只語言相當(dāng)困難，但是，經(jīng)驗(yàn)

17、表明，只學(xué)過中學(xué)數(shù)學(xué)的軟件開發(fā)人員仍然可以只用比較短的學(xué)過中學(xué)數(shù)學(xué)的軟件開發(fā)人員仍然可以只用比較短的時(shí)間就學(xué)會(huì)編寫時(shí)間就學(xué)會(huì)編寫Z規(guī)格說明。規(guī)格說明。(5) 使用使用Z語言可以降低軟件開發(fā)費(fèi)用。語言可以降低軟件開發(fā)費(fèi)用。 (6) 雖然用戶無法理解用雖然用戶無法理解用Z寫的規(guī)格說明，但是，可以依寫的規(guī)格說明，但是，可以依據(jù)據(jù)Z規(guī)格說明用自然語言重寫規(guī)格說明。規(guī)格說明用自然語言重寫規(guī)格說明。小結(jié)：小結(jié)：n基于數(shù)學(xué)的形式化規(guī)格說明技術(shù)，目前還沒有基于數(shù)學(xué)的形式化規(guī)格說明技術(shù)，目前還沒有在軟件產(chǎn)業(yè)界廣泛應(yīng)用，但它確實(shí)有實(shí)質(zhì)性的在軟件產(chǎn)業(yè)界廣泛應(yīng)用，但它確實(shí)有實(shí)質(zhì)性的優(yōu)點(diǎn)：形式化的規(guī)格說明可以用數(shù)學(xué)方法研究、優(yōu)點(diǎn)：形式化的規(guī)格說明可以用數(shù)學(xué)方法