軟件工程第4章

1、西安電子科技大學(xué)課程,第四章 形式化說(shuō)明技術(shù)JSZX.XIDIAN.EDU.CN計(jì)算機(jī)信息應(yīng)用研究中心,第四章 形式化說(shuō)明技術(shù),按照形式化的程度，可以把軟件工程使用的方法劃分成非形式化、半形式化和形式化3類(lèi)。用自然語(yǔ)言描述需求規(guī)格說(shuō)明，是典型的非形式化方法。用數(shù)據(jù)流圖或?qū)嶓w－聯(lián)系圖建立模型，是典型的半形式化方法。 所謂形式化方法，是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)，也就是說(shuō)，如果一種方法有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)，那么它就是

2、形式化的。4. 1 概述 4. 1. 1 非形式化方法的缺點(diǎn) 用自然語(yǔ)言書(shū)寫(xiě)的系統(tǒng)規(guī)格說(shuō)明書(shū)，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問(wèn)題。,第四章 形式化說(shuō)明技術(shù),所謂矛盾是指一組相互沖突的陳述。 二義性是指讀者可以用不同方式理解的陳述。 不完整性可能是在系統(tǒng)規(guī)格說(shuō)明中最常遇到的問(wèn)題之一。 抽象層次混亂是指在非常抽象的陳述中混進(jìn)了一些關(guān)于細(xì)節(jié)的低層次陳述。該規(guī)格說(shuō)明書(shū)使

3、得讀者很難了解系統(tǒng)的整體功能結(jié)構(gòu)。4. 1. 2 形式化方法的優(yōu)點(diǎn) 人在理解用自然語(yǔ)言描述的規(guī)格說(shuō)明時(shí)，容易產(chǎn)生二義性。為了克服非形式化方法的缺點(diǎn)，人們把數(shù)學(xué)引入軟件開(kāi)發(fā)過(guò)程，創(chuàng)造了基于數(shù)學(xué)的形式化方法。在開(kāi)發(fā)大型軟件系統(tǒng)的過(guò)程中應(yīng)用數(shù)學(xué)，能夠帶來(lái)下述的幾個(gè)優(yōu)點(diǎn)：,第四章 形式化說(shuō)明技術(shù),數(shù)學(xué)最有用的一個(gè)性質(zhì)是，它能夠簡(jiǎn)潔準(zhǔn)確地描述物理現(xiàn)象、對(duì)象或動(dòng)作的結(jié)果，因此是理想的建模工具。數(shù)學(xué)特別適合于表示狀態(tài)，也就是表示“做什

4、么”。需求規(guī)格說(shuō)明書(shū)主要描述應(yīng)用系統(tǒng)在運(yùn)行前和運(yùn)行后的狀態(tài)，因此，數(shù)學(xué)比自然語(yǔ)言更適合于描述詳細(xì)的需求。在理想的情況下，分析員可以寫(xiě)出系統(tǒng)的數(shù)學(xué)規(guī)格說(shuō)明書(shū)，它準(zhǔn)確到幾乎沒(méi)有二義性，而且可以用數(shù)學(xué)方法來(lái)驗(yàn)證，以發(fā)現(xiàn)存在的矛盾和不完整性，在這樣的規(guī)格說(shuō)明中完全沒(méi)有含糊性。 但是，實(shí)際情況并不這么簡(jiǎn)單，希望用少數(shù)幾個(gè)數(shù)學(xué)公式來(lái)描述它，是根本不可能的。此外，即使應(yīng)用了形式化方法，完整性也是難于保證的：由于溝通不夠，可能遺漏了客戶的一些

5、需求；規(guī)格說(shuō)明的撰寫(xiě)者可能有意省略了系統(tǒng)的某些特征，以便設(shè)計(jì)者在選擇實(shí)現(xiàn)方法時(shí)有一定自由度；要設(shè)想出使用一個(gè)大型復(fù)雜系統(tǒng)的每一個(gè)可能的情景，通常是做不到的。,第四章 形式化說(shuō)明技術(shù),在軟件開(kāi)發(fā)過(guò)程中使用數(shù)學(xué)的另一個(gè)優(yōu)點(diǎn)是，可以在不同的軟件工程活動(dòng)之間平滑地過(guò)渡。不僅功能規(guī)格說(shuō)明，而且系統(tǒng)設(shè)計(jì)也可以用數(shù)學(xué)表達(dá)。 數(shù)學(xué)作為軟件開(kāi)發(fā)工具的最后一個(gè)優(yōu)點(diǎn)是，它提供了高層確認(rèn)的手段?？梢允褂脭?shù)學(xué)方法證明，設(shè)計(jì)符合規(guī)格說(shuō)明，程序代碼正確地

6、實(shí)現(xiàn)了設(shè)計(jì)結(jié)果。,第四章 形式化說(shuō)明技術(shù),形式化規(guī)格說(shuō)明語(yǔ)言構(gòu)成：1、語(yǔ)法：一般基于集合論、數(shù)理邏輯或代數(shù)學(xué)。 2、語(yǔ)義：是其所有語(yǔ)法符號(hào)的意義的數(shù)學(xué)描述。經(jīng)典的語(yǔ)義定義方法包括指稱語(yǔ)義、代數(shù)語(yǔ)義和操作語(yǔ)義方法。 3、推演規(guī)則：一般預(yù)期數(shù)學(xué)基礎(chǔ)和語(yǔ)義定義方法密切相關(guān)。規(guī)則必須在規(guī)格說(shuō)明語(yǔ)言的語(yǔ)義系統(tǒng)中可證。因此，可以認(rèn)為規(guī)則是派生的語(yǔ)義定義，它們可以直接應(yīng)用于軟件規(guī)格說(shuō)明的性質(zhì)證明并簡(jiǎn)化推演過(guò)程。,第四章 形式化說(shuō)明技術(shù),4

7、. 1. 3 應(yīng)用形式化方法的準(zhǔn)則 人們對(duì)形式化方法的看法并不一致。為了更好地發(fā)揮這種方法的長(zhǎng)處，下面給出應(yīng)用形式化方法的幾條準(zhǔn)則，供讀者在實(shí)際工作中使用。 (1)應(yīng)該選用適當(dāng)?shù)谋硎痉椒?。通常，一種規(guī)格說(shuō)明技術(shù)只能用自然的方式說(shuō)明某一類(lèi)概念，如果用這種技術(shù)描述其不適應(yīng)于描述的概念，則不僅工作量大而且描述方式也很復(fù)雜。例如，Z語(yǔ)言并不適于說(shuō)明并發(fā)性。因此，應(yīng)該仔細(xì)選擇一種適用于當(dāng)前項(xiàng)目的形式化說(shuō)明技術(shù)。 （2）

8、應(yīng)該形式化，但不要過(guò)分形式化。目前的形式化技術(shù)還不適于描述系統(tǒng)的每個(gè)方面。例如，示例屏幕和自然語(yǔ)言可能還是目前描述用戶界面的可視性的最佳方法。但是，也不能因此就認(rèn)為完全沒(méi)有必要采用形式化方法。形式化規(guī)格說(shuō)明技術(shù)要求我們非常準(zhǔn)確地描述事物，因此有助于防止含糊和誤解。,第四章 形式化說(shuō)明技術(shù),（3）應(yīng)該估算成本。為了使用形式化方法，通常需要事先進(jìn)行大量的培訓(xùn)。最好預(yù)先估算所需的成本并編入預(yù)算。 （4）應(yīng)該有形式化方法顧問(wèn)隨時(shí)提供咨

9、詢。絕大多數(shù)軟件工程師對(duì)形式化方法中使用數(shù)學(xué)和邏輯并不很熟悉，而且沒(méi)受過(guò)使用形式化方法的專業(yè)訓(xùn)練，因此，需要專家指導(dǎo)和培訓(xùn)。 （5）不應(yīng)該放棄傳統(tǒng)的開(kāi)發(fā)方法。把形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋?lái)是可能的，而且由于取長(zhǎng)補(bǔ)短往往能獲得很好的效果。 （6）應(yīng)該建立詳盡的文檔。建議使用自然語(yǔ)言注釋形式化的規(guī)格說(shuō)明書(shū)，以幫助用戶和維護(hù)人員理解系統(tǒng)。,第四章 形式化說(shuō)明技術(shù),（7）不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。形式化方法并不能保證

10、軟件的正確性，它們只不過(guò)是有助于開(kāi)發(fā)出高質(zhì)量軟件的一種手段。除了使用形式化說(shuō)明技術(shù)外，在系統(tǒng)開(kāi)發(fā)過(guò)程中仍然必須一如既往地實(shí)施其他質(zhì)量保證活動(dòng)。 （8）不應(yīng)該盲目依賴形式化方法。形式化方法并不能保證開(kāi)發(fā)出的軟件絕對(duì)正確，例如，無(wú)法用形式化方法證明從非形式化需求到形式化規(guī)格說(shuō)明的轉(zhuǎn)換是正確的，因此，必須用其他方法（例如，評(píng)審、測(cè)試）來(lái)驗(yàn)證軟件正確性。 （9）應(yīng)該測(cè)試、測(cè)試再測(cè)試。形式化方法不僅不能保證軟件系統(tǒng)絕對(duì)正確，也不能

11、證明系統(tǒng)性能和其他質(zhì)量指標(biāo)符合要求，因此，軟件測(cè)試的重要性并沒(méi)有降低。 （10）應(yīng)該重用。即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的唯一合理的方法。而且用形式化方法說(shuō)明的軟件構(gòu)件具有清晰定義的功能和接口，使得它們有更好的可重用性。,第四章 形式化說(shuō)明技術(shù),4. 1. 4 形式化方法的分類(lèi) 1、根據(jù)說(shuō)明目標(biāo)軟件系統(tǒng)的方式，形式化方法可以分為兩類(lèi)： 1）面向模型的形式化方法。面向模型的方法通過(guò)構(gòu)

12、造一個(gè)數(shù)學(xué)模型來(lái)說(shuō)明系統(tǒng)的行為。 2）面向?qū)傩缘男问交椒?。面向?qū)傩缘姆椒ㄍㄟ^(guò)描述目標(biāo)軟件系統(tǒng)的各種屬性來(lái)間接定義系統(tǒng)行為。,第四章 形式化說(shuō)明技術(shù),2、根據(jù)表達(dá)能力，形式化方法可以分為五類(lèi)： 1）基于模型的方法：通過(guò)明確定義狀態(tài)和操作來(lái)建立一個(gè)系統(tǒng)模型（使系統(tǒng)從一個(gè)狀態(tài)轉(zhuǎn)換到另一個(gè)狀態(tài)）。用這種方法雖可以表示非功能性需求（諸如時(shí)間需求），但不能很好地表示并發(fā)性。如：Z語(yǔ)言，VDM，B方法等。 2）基

13、于邏輯的方法：用邏輯描述系統(tǒng)預(yù)期的性能，包括底層規(guī)約、時(shí)序和可能性行為。采用與所選邏輯相關(guān)的公理系統(tǒng)證明系統(tǒng)具有預(yù)期的性能。用具體的編程構(gòu)造擴(kuò)充邏輯從而得到一種形式化方法，通過(guò)保持正確性的細(xì)化步驟集來(lái)開(kāi)發(fā)系統(tǒng)。如：ITL（區(qū)間時(shí)序邏輯），區(qū)段演算（DC），模態(tài)邏輯，時(shí)序邏輯，TAM（時(shí)序代理模型），RTTL（實(shí)時(shí)時(shí)序邏輯）等。,第四章 形式化說(shuō)明技術(shù),3）代數(shù)方法：通過(guò)將未定義狀態(tài)下不同的操作行為相聯(lián)系，給出操作的顯式定義。與基于模型

14、的方法相同的是，沒(méi)有給出并發(fā)的顯式表示。如：OBJ，Larch族代數(shù)規(guī)約語(yǔ)言等； 4）過(guò)程代數(shù)方法：通過(guò)限制所有容許的可觀察的過(guò)程間通信來(lái)表示系統(tǒng)行為。此類(lèi)方法允許并發(fā)過(guò)程的顯式表示。如：通信順序過(guò)程（CSP），通信系統(tǒng)演算（CCS），通信過(guò)程代數(shù)（ACP），時(shí)序排序規(guī)約語(yǔ)言（LOTOS），計(jì)時(shí)CSP(TCSP），通信系統(tǒng)計(jì)時(shí)可能性演算（TPCCS）等。 5）基于網(wǎng)絡(luò)的方法：由于圖形化表示法易于理解，而且非專

15、業(yè)人員能夠使用，因此是一種通用的系統(tǒng)確定表示法。該方法采用具有形式語(yǔ)義的圖形語(yǔ)言，為系統(tǒng)開(kāi)發(fā)和再工程帶來(lái)特殊的好處。如 Petri圖，計(jì)時(shí)Petri圖，狀態(tài)圖等。,第四章 形式化說(shuō)明技術(shù),4. 1. 5 數(shù)學(xué)預(yù)備知識(shí) 1、集合和構(gòu)造規(guī)約 集合是對(duì)象或元素的聚集。集合論是形式化方法的基礎(chǔ)，集合中包含的元素是唯一的（即不允許重復(fù)）。具有少量的元素的集合用花括號(hào)（{，}）括起來(lái)，元素之間用逗號(hào)分開(kāi)。例如：

16、 {7，14，3，12} ；包含4個(gè)自然數(shù)的集合 {7，14，7，3，12} ；該數(shù)的聚集不是集合，因?yàn)橛?重復(fù)。 集合中的元素出現(xiàn)的順序是不重要的，集合中元素的數(shù)量稱為集合的基數(shù)，操作符#返回集合的基數(shù)，例如： #{7，14，3，12} = 4 ；其結(jié)果指出集合中項(xiàng)的數(shù)量。 有兩種定義集合的方式，一是通過(guò)枚舉出集合的元素來(lái)定義，二是創(chuàng)建一個(gè)構(gòu)造性集合規(guī)約，用布爾表

17、達(dá)式來(lái)刻劃集合成員的一般形式。因?yàn)榧弦?guī)約可以為大集合提供簡(jiǎn)潔的定義，比枚舉方式更受到青睞。,第四章 形式化說(shuō)明技術(shù),例如，{n:N|n<3●n} 規(guī)約有三部分，基調(diào)n:N，一個(gè)謂詞n<3，以及一個(gè)項(xiàng)n。 基調(diào)刻劃在形成集合時(shí)考慮的值的范圍； 謂詞（布爾表達(dá)式）定義集合如何被構(gòu)造； 項(xiàng)則指出集合中項(xiàng)的一般形式。 N表示自然數(shù)，謂詞指出只有小于3的自然數(shù)被包含在集合

18、；項(xiàng)規(guī)定集合中每個(gè)元素的形式為n。 {0，1，2} ；集合形式是明顯的，則項(xiàng)可以省略。 上面的集合可表示為： {n:N|n<3},第四章 形式化說(shuō)明技術(shù),集合元素可以是對(duì)，三元組，例如，集合定義為： { x , y:N| x +y = 10 *(x , y*2)}; 例如，第二個(gè)元素比第一個(gè)元素大3,并且第一個(gè)元素大于120，規(guī)約為：

19、 { n ：N| n > 120 *( n , n+3 )}; 當(dāng)然，表示某些計(jì)算機(jī)軟件成分所需的構(gòu)造性集合規(guī)約將比上面的例子復(fù)雜得多，然而，其基本形式和結(jié)構(gòu)是相同的。 2、集合的運(yùn)算符 運(yùn)算符∈用于表示集合中的成員關(guān)系。 例如，如果x是集合X中的成員，表達(dá)式x ∈ X 的值為真，否則其值為假。 謂詞：12 ∈{ 6，1，12，22 } 值為真，因?yàn)?2 是集合中的成員。,第四

20、章 形式化說(shuō)明技術(shù),運(yùn)算符∈的反是運(yùn)算符 如果x不是集合X的成員，表達(dá)式 x X的值為真，否則其值為假。 謂詞：13 ∈{ 6，1，13，122 } 值為假。 一個(gè)特殊的集合是空集φ，對(duì)應(yīng)普通數(shù)學(xué)中的0，空集具有它是所有集合的子集的性質(zhì)，兩個(gè)涉及空集的有用的等式是，對(duì)任何集合A： φ∪A=A和φ∩A=φ,,,第四章 形式化說(shuō)明技術(shù),1．集合的交 由集合A和集合B的共同元

21、素組成的集合，叫做A與B的交集。寫(xiě)作A∩B。 例如： （1）{3，6，9，12，15}∩{5，10，15，20，25}＝{15} （2）{二年級(jí)男生}∩{二年級(jí)三好學(xué)生}＝{二年級(jí)的男三好學(xué)生}用韋恩圖表示如下：（陰影部分表示交集） 如果集合A和集合B（都不是空集）沒(méi)有共同的元素。即A∩B＝ Ф ，我們就說(shuō)A與B是不相交集。 例如：{1，3，5，7，9}∩{2，4，6，8，10}＝ Ф,第四

22、章 形式化說(shuō)明技術(shù),2．集合的并 兩個(gè)集合A、B中的元素合在一起組成的新集合，叫做A與B的并集。寫(xiě)作A∪B。 這里要注意，若A、B有共同的元素，只列舉一次。例如： A＝{數(shù)學(xué)小組同學(xué)}＝{李明，王平，張紅，宋軍} B＝{航模小組同學(xué)}＝{張紅，宋軍，何光，方強(qiáng)，劉華} A∪B＝{數(shù)學(xué)小組同學(xué)}∪{航模小組同學(xué)}　　 ＝{李明，王平，張紅，宋軍，何光，方強(qiáng)，劉華}用韋恩圖表示如下：（劃線部分

23、表示并集）,第四章 形式化說(shuō)明技術(shù),若A、B是不相交的集，這兩個(gè)集合所有的元素合在一起就是它們的并集。 例如：{1，3，5，7}∪{2，4，6}＝{1，2，3，4，5，6，7} 從集合的觀點(diǎn)來(lái)看，加法運(yùn)算就是求兩個(gè)不相交集的并集的基數(shù)。 例如，4＋3＝7。兩個(gè)不相交集的基數(shù)都叫做加數(shù)，加法的運(yùn)算符號(hào)叫做加號(hào)。加得的結(jié)果，即兩個(gè)集的并集的基數(shù)，叫做和。,第四章 形式化說(shuō)明技術(shù),序列是一種數(shù)學(xué)結(jié)構(gòu)

24、，對(duì)元素是有序的這一事實(shí)建模。 一個(gè)序列s是對(duì)的集合，它的元素從1到最高的數(shù)排序，例如：｛(1，Jones)，(2，Wilson)，(3，Shapiro)，(4，Estavez)｝ 形成對(duì)的第一個(gè)元素的項(xiàng)總稱為序列的定義域，第二個(gè)元素總稱為序列的值域。本書(shū)中序列用尖括號(hào)指明。例如，上面的序列寫(xiě)作： ＜Jones，Wilson，Shapiro，Estavez＞ 和集合不同，序列中允許元素的重復(fù)，且序列的順序是重要

25、的。這樣有，〈Jones，Wilson，Shapiro〉≠〈Jones，Shapiro，Wilson〉和〈Jones， Wilson，Wilson〉≠〈Jones， Wilson〉 空序列表示為〈〉。 就集合而言還有集合的差，包含操作，子集等等；在形式化規(guī)約中同樣用到一組序列運(yùn)算符。希望大家在實(shí)際工作之中用到時(shí)，能夠記得這些數(shù)學(xué)的基本概念和方法。,第四章 形式化說(shuō)明技術(shù),4. 2 有窮狀態(tài)機(jī)

26、 4.2.1 概念 利用有窮狀態(tài)機(jī)可以準(zhǔn)確地描述一個(gè)系統(tǒng)，因此它是表達(dá)規(guī)格說(shuō)明的一種形式化方法。 下面通過(guò)一個(gè)簡(jiǎn)單的例子介紹有窮狀態(tài)機(jī)的基本概念。 一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)記為1、2、3，轉(zhuǎn)盤(pán)可向左（L）或向右（R）轉(zhuǎn)動(dòng)。這樣，在任意時(shí)刻轉(zhuǎn)盤(pán)都有6種可能的運(yùn)動(dòng)，即1L、1R、2L、2R、3L和3R。保險(xiǎn)箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤(pán)的任何其他運(yùn)動(dòng)都將引起報(bào)警

27、。,第四章 形式化說(shuō)明技術(shù),教材P68頁(yè)圖4.1是一個(gè)有窮狀態(tài)機(jī)的狀態(tài)轉(zhuǎn)換圖。狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述，教材P68表4.1的表格形式也可以表達(dá)同樣的信息。除了兩個(gè)終態(tài)之外，保險(xiǎn)箱的其他狀態(tài)將根據(jù)轉(zhuǎn)盤(pán)的轉(zhuǎn)動(dòng)方式轉(zhuǎn)到下一個(gè)狀態(tài)。 從上面這個(gè)簡(jiǎn)單例子可以看出，一個(gè)有窮狀態(tài)機(jī)包括下述5個(gè)部分：對(duì)于保險(xiǎn)箱的例子，相應(yīng)的有窮狀態(tài)機(jī)的各部分如下。 狀態(tài)集J：{保險(xiǎn)箱鎖定，A，B，保險(xiǎn)箱解鎖，報(bào)警}。 輸入集K：

28、{1L,1R,2L,2R,3L,3R }。 轉(zhuǎn)換函數(shù)T：由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個(gè)狀態(tài)（次態(tài)），如表4.1所示。 初始態(tài)S：保險(xiǎn)箱鎖定。 終態(tài)集F：{保險(xiǎn)箱解鎖，報(bào)警}。,第四章 形式化說(shuō)明技術(shù),一個(gè)有窮狀態(tài)機(jī)可以表示為一個(gè)5元組（J,K,T,S,T）, 其中： J 是一個(gè)有窮的非空狀態(tài)集； K 是一個(gè)有窮的非空輸入集； T 是一個(gè)從（J-F）*K到J的轉(zhuǎn)換函數(shù)；

29、 S ? J，是一個(gè)初始狀態(tài)； F J，是終態(tài)集。 有窮狀態(tài)機(jī)的概念在計(jì)算機(jī)系統(tǒng)中應(yīng)用得非常廣泛。例如，每個(gè)菜單驅(qū)動(dòng)的用戶界面都是一個(gè)有窮狀態(tài)機(jī)的實(shí)現(xiàn)。一個(gè)菜單的顯示和一個(gè)狀態(tài)相對(duì)應(yīng)，鍵盤(pán)輸入或用鼠標(biāo)選擇一個(gè)圖標(biāo)是使系統(tǒng)進(jìn)入其它狀態(tài)的一個(gè)事件。狀態(tài)的每個(gè)轉(zhuǎn)換都具有下面的形式： 當(dāng)前狀態(tài)［菜單］＋事件［所選擇的項(xiàng)］＝>下個(gè)狀態(tài)。 為了對(duì)一個(gè)系統(tǒng)進(jìn)行規(guī)格說(shuō)明,引入謂詞集P，從而把有窮狀態(tài)機(jī)擴(kuò)展為一個(gè)6

30、元組，其中每個(gè)謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。轉(zhuǎn)換函數(shù)T現(xiàn)在是一個(gè)從（J-F）*K*P到J的函數(shù)?，F(xiàn)在的轉(zhuǎn)換規(guī)則形式如下： 當(dāng)前狀態(tài)［菜單］＋事件［所選擇的項(xiàng)］＋謂詞 = >下個(gè)狀態(tài),第四章 形式化說(shuō)明技術(shù),4.2.2 例子 首先給出用自然語(yǔ)言描述的對(duì)電梯系統(tǒng)的需求： 在一幢m層的大廈中需要一套控制n部電梯的產(chǎn)品，要求這n部電梯按照約束條件C1，C2和C3在樓層間移動(dòng)。 C1：每部電梯內(nèi)有m個(gè)按鈕，

31、每個(gè)按鈕代表一個(gè)樓層。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，同時(shí)電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時(shí)指示燈熄滅。 C2：除了大廈的最低層和最高層之外，每層樓都有兩個(gè)按鈕分別請(qǐng)求電梯上行和下行。這兩個(gè)按鈕之一被按下時(shí)相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時(shí)燈熄滅，電梯向要求的方向移動(dòng)。 C3：當(dāng)對(duì)電梯沒(méi)有請(qǐng)求時(shí)，它關(guān)門(mén)并停在當(dāng)前樓層。 現(xiàn)在使用一個(gè)擴(kuò)展的有窮狀態(tài)機(jī)對(duì)本產(chǎn)品進(jìn)行規(guī)格說(shuō)明。這個(gè)問(wèn)題中有兩個(gè)按鈕集:電梯按鈕

32、和樓層按鈕。,第四章 形式化說(shuō)明技術(shù),電梯按鈕的狀態(tài)轉(zhuǎn)換圖如圖4.2所示。令EB(e,f)表示按下電梯e內(nèi)的按鈕并請(qǐng)求到f層去。EB(e,f)有兩個(gè)狀態(tài)，分別是按鈕發(fā)光(打開(kāi))和不發(fā)光(關(guān)閉)。更精確地說(shuō)，狀態(tài)是： EBON(e,f)：電梯按鈕(e,f)打開(kāi) EBOFF(e,f)：電梯按鈕(e,f)關(guān)閉 如果電梯按鈕(e,f)發(fā)光且電梯到達(dá)f層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時(shí)，按鈕將發(fā)光

33、。上述描述中包含了兩個(gè)事件，它們分別是： 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層 如果電梯按鈕(e,f)處于關(guān)閉狀態(tài)〔當(dāng)前狀態(tài)〕，而且電梯按鈕(e,f)被按下〔事件〕，而且電梯e不在f層〔謂詞〕，則該電梯按鈕打開(kāi)發(fā)光〔下個(gè)狀態(tài)〕。

34、狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下： EBOFF(e,f)+EBP(e,f)+not V(e,f) EBON(e,f) 反之，如果電梯到達(dá)f層，而且電梯按鈕是打開(kāi)的，于是它就會(huì)熄滅。這條轉(zhuǎn)換規(guī)則可以形式化地表示為： EBON(e,f)+EAF(e,f)EBOFF(e,f),第四章 形式化說(shuō)明技術(shù),圖4.2 電梯按鈕的狀態(tài)轉(zhuǎn)換圖圖4.3樓層按鈕的狀態(tài)轉(zhuǎn)換圖,第四章 形式化說(shuō)明技術(shù),接下來(lái)考慮

35、樓層按鈕。令FB(d,f)表示f層請(qǐng)求電梯向d方向運(yùn)動(dòng)的按鈕，樓層按鈕FB(d,f)的狀態(tài)轉(zhuǎn)換圖如圖4.3所示。 樓層按鈕的狀態(tài)如下： FBON(d,f)：樓層按鈕(d,f)打開(kāi) FBOFF(d,f)：樓層按鈕(d,f)關(guān)閉 如果樓層按鈕已經(jīng)打開(kāi)，而且一部電梯到達(dá)f層，則按鈕關(guān)閉。反之，如果樓層按鈕原來(lái)是關(guān)閉的，被按下后該按鈕將打開(kāi)。這段敘述中包含了以下兩個(gè)事件。 FBP(d,f)：樓層按鈕(d

36、,f)被按下 EAF(1…n,f)：電梯1或…或n到達(dá)f層 其中1…n表示或?yàn)?或?yàn)?…或?yàn)閚。,第四章 形式化說(shuō)明技術(shù),為了定義與這些事件和狀態(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=D)或待定(d=N)。 這個(gè)謂詞實(shí)際上是一個(gè)狀態(tài)，形式化方法允許把事件和狀態(tài)作為謂詞對(duì)待。使

37、用謂詞S(d,e,f)，形式化轉(zhuǎn)換規(guī)則為： FBOFF(d,f)+FBP(d,f)+not S(d,1…n,f)FBON(d,f) FBON(d,f)+EAF(1…n,f)+S(d,1…n,f)FBOFF(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)的電梯，則該樓層按鈕打開(kāi)。反之，如果樓

38、層按鈕已經(jīng)打開(kāi)，且至少有一部電梯到達(dá)f層，該部電梯將朝d方向運(yùn)動(dòng)，則按鈕將關(guā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),第四章 形式化說(shuō)明技術(shù),定義電梯按鈕和樓層按鈕的狀態(tài)都是很簡(jiǎn)單、直觀的事情?，F(xiàn)在轉(zhuǎn)向討論電梯的狀態(tài)及其轉(zhuǎn)換規(guī)則，就會(huì)出現(xiàn)一些復(fù)雜的情況。一個(gè)電梯狀態(tài)實(shí)質(zhì)上包含許多子狀

39、態(tài)。 下面定義電梯的3個(gè)狀態(tài)： M(d,e,f)：電梯e正沿d方向移動(dòng)，即將到達(dá)的是第f層 S(d,e,f)：電梯e停在f層，將朝d方向移動(dòng)(尚未關(guān)門(mén)) W(e,f)：電梯e在f層等待(已關(guān)門(mén)) 其中S(d,e,f)狀態(tài)已在討論樓層按鈕時(shí)定義過(guò)，但是，現(xiàn)在的定義更完備一些。 圖4.4是電梯的狀態(tài)轉(zhuǎn)換圖。3個(gè)電梯停止?fàn)顟B(tài)S(U,e,f)、S(N,e,f)和S(D,e,f

40、)已被組合成一個(gè)大的狀態(tài)，這樣做的目的是減少狀態(tài)總數(shù)以簡(jiǎn)化流圖。 圖4.4中包含了下述3個(gè)可觸發(fā)狀態(tài)發(fā)生改變的事件。 DC(e,f)：電梯e在樓層f關(guān)上門(mén) ST(e,f)：電梯e靠近f層時(shí)觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下 RL：電梯按鈕或樓層按鈕被按下進(jìn)入打開(kāi)狀態(tài)，登錄需求,第四章 形式化說(shuō)明技術(shù),圖4.4 電梯的狀態(tài)轉(zhuǎn)換圖,第四章 形式化說(shuō)明技術(shù),最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則

41、。為簡(jiǎn)單起見(jiàn)，這里給出的規(guī)則僅發(fā)生在關(guān)門(mén)之時(shí)。 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) 第一條規(guī)則表明，如果電梯e停在f層準(zhǔn)備向上移動(dòng)，且門(mén)已經(jīng)關(guān)閉，則電梯將向上一樓層移動(dòng)。第二條和第三條規(guī)則，分別對(duì)應(yīng)于電梯即將下降或者沒(méi)有待處理的請(qǐng)求的情況。,第四章 形式化說(shuō)明技術(shù),4. 2.3評(píng)

42、價(jià) 有窮狀態(tài)機(jī)方法采用了一種簡(jiǎn)單的格式來(lái)描述規(guī)格說(shuō)明： 當(dāng)前狀態(tài)+事件+謂詞下個(gè)狀態(tài) 這種形式的規(guī)格說(shuō)明易于書(shū)寫(xiě)、易于驗(yàn)證，而且可以比較容易地把它轉(zhuǎn)變成設(shè)計(jì)或程序代碼。事實(shí)上，可以開(kāi)發(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ō)明生成新版本的產(chǎn)品。 有窮狀態(tài)機(jī)方法比數(shù)據(jù)流圖技術(shù)更

43、精確，而且和它一樣易于理解。不過(guò)，它也有缺點(diǎn)：在開(kāi)發(fā)一個(gè)大系統(tǒng)時(shí)三元組(即狀態(tài)、事件、謂詞)的數(shù)量會(huì)迅速增長(zhǎng)。此外，和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機(jī)方法也沒(méi)有處理定時(shí)需求。下節(jié)將介紹的Petri網(wǎng)技術(shù)，是一種可處理定時(shí)問(wèn)題的形式化方法。,第四章 形式化說(shuō)明技術(shù),4. 3　Petri網(wǎng) 4. 3. 1概念 并發(fā)系統(tǒng)中遇到的一個(gè)主要問(wèn)題是定時(shí)問(wèn)題．這個(gè)問(wèn)題可以表現(xiàn)為多種形式，如同步問(wèn)題﹑競(jìng)爭(zhēng)條件以及死鎖問(wèn)題．定時(shí)問(wèn)題通

44、常是由不好的設(shè)計(jì)或者有錯(cuò)誤的實(shí)現(xiàn)引起的，而這些的設(shè)計(jì)和實(shí)現(xiàn)通常又是由不好的規(guī)格說(shuō)明造成的．如果規(guī)格說(shuō)明不當(dāng)，則有導(dǎo)致不完善的設(shè)計(jì)或?qū)崿F(xiàn)的危險(xiǎn)．用于確定系統(tǒng)中隱含的定時(shí)問(wèn)題的一種有效技術(shù)是Petri網(wǎng)，這種技術(shù)的一個(gè)很大的優(yōu)點(diǎn)是它也可以用于設(shè)計(jì)中． Petri網(wǎng)是由Carl　Adam　Petri發(fā)明的．最初只有自動(dòng)化專家對(duì)Petri網(wǎng)感興趣，后來(lái)Petri網(wǎng)在計(jì)算機(jī)科學(xué)中也得到廣泛的應(yīng)用，例如，在性能評(píng)價(jià)﹑操作系統(tǒng)和軟件工程等領(lǐng)域

45、，Petri網(wǎng)應(yīng)用得都比較廣泛．特別是已經(jīng)證明，用Petri網(wǎng)可以有效地描述并發(fā)活動(dòng)．,第四章 形式化說(shuō)明技術(shù),Petri網(wǎng)包含４種元素：一組位置P﹑一組轉(zhuǎn)換T﹑輸入函數(shù)I和輸出函數(shù)O。教材P72圖４.５舉例說(shuō)明了Petri網(wǎng)的組成．其中， 一組位置P，在圖中用圓圈代表位置． 一組轉(zhuǎn)換T，在圖中用短直線表示轉(zhuǎn)換． 兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是： I(t1)= {P2，P4}

46、 I(t2)= {P2} 兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)，用有轉(zhuǎn)換指向位置的箭頭表示，它們是： O（t1）={P1} O（t2）={P3，P3} 注意輸出函數(shù)O(t2)中有兩個(gè) P3，是因?yàn)橛袃蓚€(gè)箭頭有t2指向P3。,第四章 形式化說(shuō)明技術(shù),更形式化的Petri網(wǎng)結(jié)構(gòu)，是一個(gè)四元組C=(P,T,I,O)。其中， P={P1，...，Pn}是一個(gè)有窮位置集，n>=0。

47、 T={t1，...，tm}是一個(gè)有窮轉(zhuǎn)換集，m>=0，且T和P不相交。 I：T→P∞為輸入函數(shù)，是由轉(zhuǎn)換到位置無(wú)序單位組（bags）的映射。 O：T→P∞為輸出函數(shù)，是由轉(zhuǎn)換到位置無(wú)序單位組的映射。 一個(gè)無(wú)序單位組或多重組是允許一個(gè)元素有多個(gè)實(shí)例的廣義集。 Petri網(wǎng)的標(biāo)記是在Petri網(wǎng)中權(quán)標(biāo)（token）的分配。例如，在教材P73圖4.6中有4個(gè)權(quán)標(biāo)，其中一個(gè)在P1

48、中，兩個(gè)在P2中，P3中沒(méi)有，還有一個(gè)在P4中。上述標(biāo)記可以用向量（1，2，0，1）表示。由于P2和P4中有權(quán)標(biāo)，因此t1啟動(dòng)（即被激發(fā)）。通常，當(dāng)每個(gè)輸入位置所擁有的權(quán)標(biāo)數(shù)大于等于從該位置到轉(zhuǎn)換的線數(shù)時(shí)，就允許轉(zhuǎn)換。當(dāng)t1被激發(fā)時(shí)，P2和P4上各有一個(gè)權(quán)標(biāo)被移出，P1上增加一個(gè)權(quán)標(biāo)。Petri網(wǎng)中權(quán)標(biāo)總數(shù)不是固定的，在這個(gè)例子中兩個(gè)權(quán)標(biāo)被移出，而P1上只能增加一個(gè)權(quán)標(biāo)。,第四章 形式化說(shuō)明技術(shù),圖4.6 帶標(biāo)記的Petri網(wǎng)

49、 圖4.7 圖4.6的Petri網(wǎng)在轉(zhuǎn)換 t1被激發(fā)后的情況圖4.8 圖4.7的Petri網(wǎng)在轉(zhuǎn)換 t2被激發(fā)后的情況 圖4.9 含禁止線的Petri網(wǎng),第四章 形式化說(shuō)明技術(shù),教材P73頁(yè)圖4.6中P2上有權(quán)標(biāo)，因此t2也可以被激發(fā)。當(dāng)t2被激發(fā)時(shí)，P2上將移走一個(gè)權(quán)標(biāo)，而P3上新增加兩

50、個(gè)權(quán)標(biāo)。Petri網(wǎng)具有非確定性，也就是說(shuō)，如果數(shù)個(gè)轉(zhuǎn)換都達(dá)到了激發(fā)條件，則其中任意一個(gè)都可以被激發(fā)。 教材P73頁(yè)圖4.6所示Petri網(wǎng)的標(biāo)記為（1，2，0，1），t1和t2都可以被激發(fā)。假設(shè)t1被激發(fā)了，則結(jié)果如圖4.7所示，標(biāo)記為（2，1，0，0）。此時(shí)，只有t2可以被激發(fā)。如果t2也被激發(fā)了，則權(quán)標(biāo)從P2中移出，兩個(gè)新權(quán)標(biāo)被放在P3上，結(jié)果如圖4.8所示，標(biāo)記為（2，0，2，0）。,第四章 形式化說(shuō)明技術(shù),

51、更形式化的說(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ò)充是加入禁止線。如圖4.9所示，禁止線是用一個(gè)小圓圈而不是用箭頭標(biāo)記的輸入線。通常，當(dāng)每個(gè)輸入線上至少有一個(gè)標(biāo)權(quán)，而禁止線上沒(méi)有標(biāo)權(quán)，因此轉(zhuǎn)換t1可以被激發(fā)。,第四章 形式化說(shuō)明技術(shù),

52、動(dòng)態(tài)轉(zhuǎn)移特征,網(wǎng)論的觀點(diǎn)認(rèn)為，解決沖突的辦法可以是，通過(guò)環(huán)境對(duì)系統(tǒng)進(jìn)行控制。這里有兩種可能：若t1發(fā)生，p1失去標(biāo)記，p2獲得標(biāo)記，這時(shí)只有t2可以發(fā)生，之后標(biāo)記回到p1。這時(shí)若再讓t1發(fā)生，則會(huì)重復(fù)上述過(guò)程。若讓t3發(fā)生，p1失去標(biāo)記，p3和p4同時(shí)各得一個(gè)標(biāo)記。這時(shí)t4和t5都可以發(fā)生，且互不影響，網(wǎng)論中稱這種現(xiàn)象為“并發(fā)”(concurrent)，t4和t5發(fā)生以后，t6可以發(fā)生，使標(biāo)記又回到p1，p6起著使t4和t5兩個(gè)異步活動(dòng)

53、同步的作用。,圖中的Petri網(wǎng)，只有p1中有一個(gè)標(biāo)記，從這個(gè)給定的初始標(biāo)識(shí)看，t1和t3都能發(fā)生，但不能同時(shí)發(fā)生，因?yàn)樗鼈児蚕韕1中的一個(gè)資源，這種現(xiàn)象叫做“沖突”（conflict）。,第四章 形式化說(shuō)明技術(shù),如果讓p1和p3各有一個(gè)標(biāo)記，并規(guī)定位置容量均不能超過(guò)1，這時(shí)t3不能發(fā)生，因?yàn)閠3的發(fā)生會(huì)使p3的容量超過(guò)1，稱這種現(xiàn)象為“碰撞”（contact）。 有時(shí)，一個(gè)Petri網(wǎng)中同時(shí)存在著并發(fā)和沖突，而且并發(fā)的實(shí)施

54、會(huì)引起沖突的消失（減少）或出現(xiàn)（增加），我們稱這種情況為“混惑”（confusion）。,在圖示Petri網(wǎng)中，t1和t3是兩個(gè)并發(fā)事件，如果t1實(shí)際上在t3之前發(fā)生，則t2不會(huì)發(fā)生沖突；反之，則發(fā)生沖突。所以存在著“混惑”的系統(tǒng)是不好的系統(tǒng)，因?yàn)樵谶@種系統(tǒng)中，沖突忽隱忽現(xiàn)，使得外部環(huán)境對(duì)系統(tǒng)難以控制。,第四章 形式化說(shuō)明技術(shù),4.3.2 例子 現(xiàn)在把Petri網(wǎng)應(yīng)用于上一節(jié)討論過(guò)的電梯問(wèn)題。當(dāng)用Petri網(wǎng)表示電梯系

55、統(tǒng)的規(guī)格說(shuō)明時(shí)，每個(gè)樓層用一個(gè)位置Ff代表(1≤f≤m)，在Petri網(wǎng)中電梯是用一個(gè)權(quán)標(biāo)代表的。在位置Ff上有權(quán)標(biāo)，表示在樓層f上有電梯。 1. 電梯按鈕 電梯問(wèn)題的第一個(gè)約束條件描述了電梯按鈕的行為，現(xiàn)在復(fù)述一下這個(gè)約束條件。 第一條約束C1：每部電梯有m個(gè)按鈕，每層對(duì)應(yīng)一個(gè)按鈕。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當(dāng)電梯到達(dá)指定的樓層時(shí)，按鈕將熄滅。,第四章 形式化說(shuō)明技術(shù),為了用Pet

56、ri網(wǎng)表達(dá)電梯按鈕的規(guī)格說(shuō)明，在Petri網(wǎng)中還必須設(shè)置其他的位置。電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示(1≤f≤m)。在EBf上有一個(gè)權(quán)標(biāo)，就表示電梯內(nèi)樓層f的按鈕被按下了。 電梯按鈕只有在第一次被按下時(shí)才會(huì)由暗變亮，以后再按它則只會(huì)被忽略。圖4.10所示的Petri網(wǎng)準(zhǔn)確地描述了電梯按鈕的行為規(guī)律。首先，假設(shè)按鈕沒(méi)有發(fā)亮，顯然在位置EBf上沒(méi)有權(quán)標(biāo)，從而在存在禁止線的情況下，轉(zhuǎn)換“EBf被按下”是允許發(fā)生的

57、。假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)換被激發(fā)并在EBf上放置了一個(gè)權(quán)標(biāo)，如圖4.10所示。以后不論再按下多少次按鈕，禁止線與現(xiàn)有權(quán)標(biāo)的組合都決定了轉(zhuǎn)換“EBf被按下”不能再被激發(fā)了，因此，位置EBf上的權(quán)標(biāo)數(shù)不會(huì)多于1。,第四章 形式化說(shuō)明技術(shù),圖4.10 Petri網(wǎng)表示的電梯按鈕,第四章 形式化說(shuō)明技術(shù),假設(shè)電梯由g層駛向f層，因?yàn)殡娞菰趃層，如圖4.10所示，位置Fg上有一個(gè)權(quán)標(biāo)。由于每條輸入線上各有一個(gè)權(quán)標(biāo)，轉(zhuǎn)換“電梯在運(yùn)行”被激發(fā)，從

58、而EBf和Fg上的權(quán)標(biāo)被移走，按鈕EBf被關(guān)閉，在位置Ff上出現(xiàn)一個(gè)新權(quán)標(biāo)，即轉(zhuǎn)換的激發(fā)使電梯由g層駛到f層。 事實(shí)上，電梯由g層移到f層是需要時(shí)間的，為處理這個(gè)情況及其他類(lèi)似的問(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)系。,第四章 形式化說(shuō)明技術(shù),2. 樓層按鈕

59、 在第二個(gè)約束條件中描述了樓層按鈕的行為。 第二條約束C2：除了第一層與頂層之外，每個(gè)樓層都有兩個(gè)按鈕，一個(gè)要求電梯上行，另一個(gè)要求電梯下行。這些按鈕在按下時(shí)發(fā)亮，當(dāng)電梯到達(dá)該層并將向指定方向移動(dòng)時(shí)，相應(yīng)的按鈕才會(huì)熄滅。 在Petri網(wǎng)中樓層按鈕用位置FBfu和FBfd表示，分別代表f樓層請(qǐng)求電梯上行和下行的按鈕。底層的按鈕為FB1u，最高層的按鈕為FBmd，中間每一層有兩個(gè)按鈕FBfu和FBfd(1＜f＜m)。,第四

60、章 形式化說(shuō)明技術(shù),圖4.11 Petri網(wǎng)表示樓層按鈕,第四章 形式化說(shuō)明技術(shù),圖4.11所示的情況為電梯由g層駛向f層。根據(jù)電梯乘客的要求，某一個(gè)樓層按鈕亮或兩個(gè)樓層按鈕都亮。如果兩個(gè)按鈕都亮了，則只有一個(gè)按鈕熄滅。圖4.11所示的Petri網(wǎng)可以保證，當(dāng)兩個(gè)按鈕都亮了的時(shí)候，只有一個(gè)按鈕熄滅。但是要保證按鈕熄滅正確，則需要更復(fù)雜的Petri網(wǎng)模型。 最后，考慮第三條約束。 第三條約束C3：當(dāng)電梯沒(méi)有收到請(qǐng)求時(shí)，

61、它將停留在當(dāng)前樓層并關(guān)門(mén)。 這條約束很容易實(shí)現(xiàn)，如圖4.11所示，當(dāng)沒(méi)有請(qǐng)求(FBfu和FBfd上無(wú)權(quán)標(biāo)）時(shí)，任何一個(gè)轉(zhuǎn)換“電梯在運(yùn)行”都不能被激發(fā)。,第四章 形式化說(shuō)明技術(shù),4.4  Z 語(yǔ)言  在形式化的規(guī)格說(shuō)明語(yǔ)言中，Z語(yǔ)言贏的了廣泛的贊譽(yù)。使用Z語(yǔ)言需要具備集合論、函數(shù)、數(shù)理邏輯等方面的知識(shí)。即使用戶已經(jīng)掌握了所需要的背景知識(shí)，Z語(yǔ)言也是相當(dāng)難學(xué)的，因?yàn)樗耸褂贸Ｓ玫募险摵蛿?shù)理邏

62、輯符號(hào)之外，還使用了一些特殊符號(hào)。4.4.1 簡(jiǎn)介 本節(jié)結(jié)合電梯問(wèn)題的例子，簡(jiǎn)要的介紹Z語(yǔ)言。 用Z語(yǔ)言描述的、最簡(jiǎn)單的形式化規(guī)格說(shuō)明含有下述4個(gè)部分： 1.給定的集合、數(shù)據(jù)類(lèi)型及常數(shù)。 2.狀態(tài)定義。 3.初始狀態(tài)。 4.操作。,第四章 形式化說(shuō)明技術(shù),1．給定的集合 一個(gè)Z規(guī)則說(shuō)明從一系列給定的初始化集合開(kāi)始。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集

63、合用帶方括號(hào)的形式標(biāo)識(shí)。對(duì)于電梯問(wèn)題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，Z規(guī)則說(shuō)明開(kāi)始于：[Button] 2．狀態(tài)定義 一個(gè)Z規(guī)則說(shuō)明有若干個(gè)“格”組成，每個(gè)格含有一組變量說(shuō)明和一系列限定變量取值范圍的謂詞。例如，格S的格式圖教材P76頁(yè)圖4.12所示。,第四章 形式化說(shuō)明技術(shù),Z格S的格式,在電梯問(wèn)題中，Button有4個(gè)子集，即floor_buttons（樓層按鈕的集合）、elev

64、ator_buttons（電梯按鈕的集合）、buttons（電梯問(wèn)題中所有按鈕的集合）以及pushed（所有被按的按鈕的的集合，即所有處于打開(kāi)狀態(tài)的按鈕的集合）。 教材P76頁(yè)圖4.13描述了格Button_State,其中，符號(hào)P表示冪集（即給定集的所有子集），約束條件聲明，floor_buttons集與elebator_buttons集不相交，共同組成buttons集（把它們放于教材P76頁(yè)圖4.13中只是用來(lái)說(shuō)明Z格包含

65、的內(nèi)容）。,第四章 形式化說(shuō)明技術(shù),3．初始狀態(tài) 抽象的初始狀態(tài)是指系統(tǒng)第一次開(kāi)啟時(shí)的狀態(tài)。對(duì)于電梯問(wèn)題來(lái)說(shuō)，抽象的初始狀態(tài)為： Button_Init＝［Button_State｜pushed= Ф ］ 上式表示，當(dāng)系統(tǒng)首次開(kāi)啟時(shí)pushed集為空，即所有按鈕都處于關(guān)閉狀態(tài)。 4．操作 如果一個(gè)原來(lái)處與關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開(kāi)啟，這個(gè)按鈕就被添加到pushed集中。教材P77

66、頁(yè)圖4.14定義了操作Push_Button（按按鈕）。Z語(yǔ)言的語(yǔ)法規(guī)定，當(dāng)一個(gè)格被用在另一個(gè)格中時(shí)，要在它前面加上三角形符號(hào)Δ作為前綴，因此，格Push_Button的第一行最前面有一個(gè)三角形符號(hào)作為格Button_State的前綴。操作Push_Button有一個(gè)輸入變量“button?”。問(wèn)號(hào)“？”表示輸入變量，而感嘆號(hào)“！”代表輸出變量。,第四章 形式化說(shuō)明技術(shù),操作的謂詞部分，包含了一組調(diào)用操作的前置條件，以及操作完全結(jié)束后

67、的后置條件。如果前置條件成立，則操作執(zhí)行完成后可得到后置條件。但是，如果在前置條件不成立的條件下調(diào)用該操作，則不能得到指定的結(jié)果。（因此結(jié)果無(wú)法預(yù)測(cè)） 教材P77頁(yè)圖4.14中的第一個(gè)前置條件規(guī)定，“button?”必須是buttons的一個(gè)元素，而buttons是電梯系統(tǒng)中所有按鈕的集合。如果第二個(gè)前置條件button? Pushed得到滿足（即按鈕沒(méi)有開(kāi)啟），則更新pushed按鈕集，使之包含剛開(kāi)啟的按鈕“but

68、ton?”。在Z語(yǔ)言中，當(dāng)一個(gè)變量的值發(fā)生改變時(shí)，就用符號(hào)“′”表示。也就是說(shuō)，后置條件是當(dāng)執(zhí)行完操作Push_Button之后，“button?”將被加入到pushed集中。無(wú)需直接打開(kāi)按鈕，只要使“button?”變成pushed中的一個(gè)元素即可。,第四章 形式化說(shuō)明技術(shù),還有一種可能性是，被按的按鈕原先已經(jīng)被打開(kāi)。由于button? ∈pushed，根據(jù)第三個(gè)前置條件，將沒(méi)有任何事情發(fā)生，這可以用pushed′=pushed來(lái)表

69、示，即pushed的新?tīng)顟B(tài)和舊狀態(tài)一樣。注意。如果沒(méi)有第三個(gè)前置條件，規(guī)格說(shuō)明將不能說(shuō)明在一個(gè)按鈕已被按過(guò)之后又被按了一次的情況下將發(fā)生什么事，因此，結(jié)果將是不可預(yù)測(cè)的。 假設(shè)電梯達(dá)到了某樓層，如果相應(yīng)的樓層按鈕已經(jīng)打開(kāi)，則此時(shí)它會(huì)關(guān)閉；同樣，如果相應(yīng)的電梯按鈕已經(jīng)打開(kāi)，則此時(shí)它會(huì)關(guān)閉。也就是說(shuō)，如果“button?”屬于pushed集，則將它移出該集合，如教材P77頁(yè)圖4.15所示（符號(hào)“\”表示集合差運(yùn)算）。但是，如果按鈕