【正文】 雖然用 Z寫規(guī)格說(shuō)明所需用的時(shí)間比使用非形式化技術(shù)要多，但開(kāi)發(fā)過(guò)程所需要的總 在 Z語(yǔ)言中，當(dāng)一個(gè)變量的值發(fā)生改變時(shí)，就用符號(hào) “’” 表示。 現(xiàn)在依次介紹這 4 1. 一個(gè) Z規(guī)格說(shuō)明從一系列給定的初始化集合開(kāi)始。當(dāng)用 Petri網(wǎng)表示電梯系統(tǒng)的規(guī)格說(shuō)明時(shí)，每個(gè)樓層用一個(gè)位置 Ff代表(1≤f≤m) ，在 Petri網(wǎng)中電梯是用一個(gè)令牌代表的。 通常，當(dāng)每個(gè)輸入位置所擁有的令牌數(shù)等于從該位置到轉(zhuǎn)換的線數(shù)時(shí)，就允許轉(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)化流圖。反之，如果樓層按鈕原來(lái)是關(guān)閉的，被按下后該按鈕將打 FBP(d,f)：樓層按鈕 (d,f) EAF(1 應(yīng)用形式化方法的準(zhǔn)則 為了更好地發(fā)揮這種方法的長(zhǎng)處，下面給出應(yīng)用形式化方法的幾條準(zhǔn)則，供讀者在實(shí)際工作中使用。 不應(yīng)該盲目依賴形式化方法，這種 圖 電梯的狀態(tài)轉(zhuǎn)換圖 圖 發(fā)生改變的事件 DC(e,f)：電梯 e在樓層 f ST(e,f)：電梯 e靠近 f層時(shí)觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下。當(dāng) t1被激發(fā)時(shí)， P2和 P4上各有一個(gè)令牌被移出，而 P1上則增加一個(gè)令牌。在位置 Ff上有令牌，表示在樓層 f 1. 為了用 Petri網(wǎng)表達(dá)電梯按鈕的規(guī)格說(shuō)明，在 Petri網(wǎng)中還必須設(shè)置其他的位置。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集合用帶方括號(hào)的形式表示。也就是說(shuō)，后置條件是當(dāng)執(zhí)行完操作 Push_Button之后，“ button?”將被加入到 pushed集中。 雖然用戶無(wú)法理解用 Z寫的規(guī)格說(shuō)明，但是，可以依據(jù) Z規(guī)格說(shuō)明用自然語(yǔ)言重寫規(guī)格說(shuō)明。 使用 Z語(yǔ)言可以降低軟件開(kāi)發(fā)費(fèi)用。如果第二個(gè)前置條件 button? pushed得到滿足 (即按鈕沒(méi)有開(kāi)啟 )，則更新 pushed按鈕集，使之包含剛開(kāi)啟的按鈕 “ button?”。 圖 含禁止線的 Petri網(wǎng) 讓我們把 Petri網(wǎng)應(yīng)用于上一節(jié)討論過(guò)的電梯問(wèn)題。由于 P2和 P4中有令牌，因此 t1啟動(dòng) (即被激發(fā) )。 圖 。 如果樓層按鈕已經(jīng)打開(kāi)，而且一部電梯到達(dá) f層，則按鈕關(guān)閉。在系統(tǒng)開(kāi)發(fā)過(guò)程中必須一如既往地實(shí)施其他 SQA活動(dòng)?？梢允褂脭?shù)學(xué)方法證明，設(shè)計(jì)符合規(guī)格說(shuō)明，程序代碼正確地反映了設(shè)計(jì)結(jié)果。 選擇適用于當(dāng)前項(xiàng)目的符號(hào)系統(tǒng)。 應(yīng)該測(cè)試、測(cè)試再測(cè)試。n,f)：電梯 1或 …或 n到達(dá) f層 其中 1 RL：電梯按鈕或樓層按鈕被按下進(jìn)入 最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。 Petri網(wǎng)中令牌總數(shù)不 是固定的，在這個(gè)例子中兩個(gè)令牌被移出，而 P1上只能增加一個(gè)令牌。電梯中樓層 f的按鈕，在 Petri網(wǎng)中用位置EBf表示 (1≤f≤m) 。對(duì)于電梯問(wèn)題，給定的初始化集合稱為 Button，即所有按鈕的集合，因此，Z 〔 Button 2. 一個(gè) Z規(guī)格說(shuō)明由若干個(gè) “ 格 (schema)”組成，每個(gè)格含有一組變量說(shuō)明和一系列限定變量取值范圍的謂詞。我們無(wú)需直接打開(kāi)按鈕，只要使 “ button?”變成 pushed 圖 操作 Push_Button的 Z規(guī)格說(shuō)明 還有一種可能性是，被按的按鈕原先已經(jīng)打開(kāi)了。經(jīng)驗(yàn)證明，這樣得到的自然語(yǔ)言規(guī)格說(shuō)明，比直接用自然語(yǔ)言寫出 使用形式化規(guī)格說(shuō)明是全球的總趨勢(shì)，過(guò)去，主要是歐洲習(xí)慣于使用形式化規(guī)格說(shuō)明技術(shù)，現(xiàn)在越來(lái)越多的美國(guó)公司也開(kāi) 小結(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) )。 雖然完全學(xué)會(huì) Z語(yǔ)言相當(dāng)困難，但是，經(jīng)驗(yàn)表明，只學(xué)過(guò)中學(xué)數(shù)學(xué)的軟件開(kāi)發(fā)人員仍然可以只用比較短的時(shí)間就學(xué)會(huì)編寫 Z規(guī)格說(shuō)明，當(dāng)然，這些人還沒(méi)有能力