軟件工程(第3版)第14章-人民郵電出版社-資料下載頁(yè)
2025-08-14 11:11本頁(yè)面
【正文】 作的前置條件，以及操作完全結(jié)束后的后置條件。如果前置條件成立，則操作執(zhí)行完成后可得到后置條件。但是，如果在前置條件不成立的情況下調(diào)用該操作，則不能得到指定的結(jié)果 (因此結(jié)果無(wú)法預(yù)測(cè) )。 圖 ，“ button?”必須是 buttons的一個(gè)元素，而 buttons是電梯系統(tǒng)中所有按鈕的集合。如果第二個(gè)前置條件 button? pushed得到滿足 (即按鈕沒(méi)有開(kāi)啟 )，則更新 pushed按鈕集，使之包含剛開(kāi)啟的按鈕 “ button?”。 在 Z語(yǔ)言中，當(dāng)一個(gè)變量的值發(fā)生改變時(shí)，就用符號(hào) “’” 表示。也就是說(shuō)，后置條件是當(dāng)執(zhí)行完操作 Push_Button之后，“ button?”將被加入到 pushed集中。我們無(wú)需直接打開(kāi)按鈕，只要使 “ button?”變成 pushed 圖 操作 Push_Button的 Z規(guī)格說(shuō)明 還有一種可能性是，被按的按鈕原先已經(jīng)打開(kāi)了。由于 button?∈pushed ，根據(jù)第三個(gè)前置條件，將沒(méi)有任何事情發(fā)生，這可以用 pushed′=pushed 來(lái)表示，即pushed的新?tīng)顟B(tài)和舊狀態(tài)一樣。 注意，如果沒(méi)有第三個(gè)前置條件，規(guī)格說(shuō)明將不能說(shuō)明在一個(gè)按鈕已被按過(guò)之后又被按了一次的情況下將發(fā)生什么事， 假設(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集，則將它移出該集合，如圖 (符號(hào) “ ＼ ” 表示集合差運(yùn)算 )。 但是，如果按鈕 “ button?”原先沒(méi)有打開(kāi)，則 pushed集合不發(fā)生變化。 本節(jié)的討論有所簡(jiǎn)化，沒(méi)有區(qū)分上行和下行樓層按鈕，但是，仍然講清了使用 Z 圖 操作 Floor_Arrival的 Z規(guī)格說(shuō)明 已經(jīng)在許多軟件開(kāi)發(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寫(xiě)的規(guī)格說(shuō)明的錯(cuò)誤，特別是在自己審查規(guī)格說(shuō)明，及根據(jù)形式化的規(guī)格說(shuō)明來(lái)審查設(shè)計(jì)與代 用 Z寫(xiě)規(guī)格說(shuō)明時(shí)，要求作者十分精確地使用 Z說(shuō)明符。由于對(duì)精確性的要求很高，從而和非形式化規(guī)格說(shuō)明相比，減 Z 是一種形式化語(yǔ)言，在需要時(shí)開(kāi)發(fā)者可以嚴(yán)格地驗(yàn)證規(guī)格說(shuō)明的正確性。 雖然完全學(xué)會(huì) Z語(yǔ)言相當(dāng)困難，但是，經(jīng)驗(yàn)表明，只學(xué)過(guò)中學(xué)數(shù)學(xué)的軟件開(kāi)發(fā)人員仍然可以只用比較短的時(shí)間就學(xué)會(huì)編寫(xiě) Z規(guī)格說(shuō)明，當(dāng)然，這些人還沒(méi)有能力 使用 Z語(yǔ)言可以降低軟件開(kāi)發(fā)費(fèi)用。雖然用 Z寫(xiě)規(guī)格說(shuō)明所需用的時(shí)間比使用非形式化技術(shù)要多，但開(kāi)發(fā)過(guò)程所需要的總 雖然用戶無(wú)法理解用 Z寫(xiě)的規(guī)格說(shuō)明，但是，可以依據(jù) Z規(guī)格說(shuō)明用自然語(yǔ)言重寫(xiě)規(guī)格說(shuō)明。經(jīng)驗(yàn)證明，這樣得到的自然語(yǔ)言規(guī)格說(shuō)明，比直接用自然語(yǔ)言寫(xiě)出 使用形式化規(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) )。 此外，形式化的規(guī)格說(shuō)明消除了二義性，而且它鼓勵(lì)軟件開(kāi)發(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)則 (見(jiàn) )，對(duì)于讀者今后在實(shí)際工作中更好地利用形式化方法，可能 本章簡(jiǎn)要地介紹了有窮狀態(tài)機(jī)、 Petri網(wǎng)和 Z語(yǔ)言等三種典型的形式化方法，使讀者對(duì)它們有初步的、概括的了解。當(dāng)然，要想在實(shí)際工作中使用這些方法，還需要
化學(xué)相關(guān)推薦
鄂ICP備17016276號(hào)-1