軟件工程(第3版)第14章-人民郵電出版社(參考版)
2024-08-25 11:11本頁面
【正文】 當(dāng)然，要想在實(shí)際工作中使用這些方法，還需要 。 把形式化方法和欠形式化方法有機(jī)地結(jié)合起來，使它們?nèi)￠L補(bǔ)短，應(yīng)該能獲得更理想的效果。 此外，形式化的規(guī)格說明消除了二義性，而且它鼓勵(lì)軟件開發(fā)者在軟件工程過程的早期階段使用更嚴(yán)格的方法，從而可 當(dāng)然，形式化方法也有缺點(diǎn)：大多數(shù)形式化的規(guī)格說明主要關(guān)注于系統(tǒng)的功能和數(shù)據(jù)，而問題的時(shí)序、控制和行為等方面的需求卻更難于表示。 雖然用戶無法理解用 Z寫的規(guī)格說明，但是，可以依據(jù) Z規(guī)格說明用自然語言重寫規(guī)格說明。 使用 Z語言可以降低軟件開發(fā)費(fèi)用。 由于對精確性的要求很高，從而和非形式化規(guī)格說明相比，減 可以比較容易地發(fā)現(xiàn)用 Z寫的規(guī)格說明的錯(cuò)誤，特別是在自己審查規(guī)格說明，及根據(jù)形式化的規(guī)格說明來審查設(shè)計(jì)與代 本節(jié)的討論有所簡化，沒有區(qū)分上行和下行樓層按鈕，但是，仍然講清了使用 Z 圖 操作 Floor_Arrival的 Z規(guī)格說明 已經(jīng)在許多軟件開發(fā)項(xiàng)目中成功地運(yùn)用了 Z語言，目前， Z也許是應(yīng)用得最廣泛的形式化語言，尤其是在大型項(xiàng)目中 Z語言的優(yōu)勢更加明顯。也就是說，如果 “ button?”屬于 pushed集，則將它移出該集合，如圖 (符號 “ ＼ ” 表示集合差運(yùn)算 )。由于 button?∈pushed ，根據(jù)第三個(gè)前置條件，將沒有任何事情發(fā)生，這可以用 pushed′=pushed 來表示，即pushed的新狀態(tài)和舊狀態(tài)一樣。也就是說，后置條件是當(dāng)執(zhí)行完操作 Push_Button之后，“ button?”將被加入到 pushed集中。如果第二個(gè)前置條件 button? pushed得到滿足 (即按鈕沒有開啟 )，則更新 pushed按鈕集，使之包含剛開啟的按鈕 “ button?”。但是，如果在前置條件不成立的情況下調(diào)用該操作，則不能得到指定的結(jié)果 (因此結(jié)果無法預(yù)測 )。 操作的謂詞部分，包含了一組調(diào)用操作的前置條件，以及操作完全結(jié)束后的后置條件。 操作 Push_Button有一個(gè)輸入變量“ button?”。圖 Push_Button(按按鈕 )。 約束條件聲明， floor_buttons集與elevator_buttons集不相交，而且它們共同組成 buttons集 (在下面的討論中并不需要 floor_buttons集和 elevator_buttons集，把它們放于圖 Z格包含的內(nèi)容 ) 圖 Z格 S的格式 圖 Z格 Button_State 3. 抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時(shí)的狀態(tài)。例如，格 S的格式如圖 在電梯問題中， Button有 4個(gè)子集，即floor_buttons(樓層按鈕的集合 )、elevator_buttons(電梯按鈕的集合 )、buttons(電梯問題中所有按鈕的集合 )以及pushed(所有被按的按鈕的集合，即所有處于打開狀態(tài)的按鈕的集合 )。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集合用帶方括號的形式表示。 底層的按鈕為 ，最高層的按鈕為 ，中間每一層有兩個(gè)按鈕 和 (1＜ f＜ m) ufFBdfFBuFB1dmFBufFB dfFB圖 Petri網(wǎng)表示樓層按鈕 第三條約束 C3：當(dāng)電梯沒有收到請求 這條約束很容易實(shí)現(xiàn)，如圖 示，當(dāng)沒有請求 ( 和 上無令牌 )時(shí)，任何一個(gè)轉(zhuǎn)換“電梯在運(yùn)行”都不能被激發(fā)。 也就是說，在標(biāo)準(zhǔn) Petri網(wǎng)中轉(zhuǎn)換是瞬時(shí)完成的，而在現(xiàn)實(shí)情況下就需要時(shí)間控制 Petri網(wǎng)，以使轉(zhuǎn)換與非零時(shí)間相聯(lián)系。以后不論再按下多少次按鈕，禁止線與現(xiàn)有令牌的組合都決定了轉(zhuǎn)換 “ EBf被按下 ”不能再被激發(fā)了，因此，位置 EBf上的令牌數(shù)不會多于 1 圖 Petri網(wǎng)表示的電梯按鈕 假設(shè)電梯由 g層駛向 f層，因?yàn)殡娞菰?g層，如圖 ，位置 Fg上有一個(gè)令牌。首先，假設(shè)按鈕沒有發(fā)亮，顯然在位置 EBf上沒有令牌，從而在存在禁止線的情況下，轉(zhuǎn)換 “ EBf被按下 ” 是允許發(fā)生的。在 EBf上有一個(gè)令牌，就表示電梯內(nèi)樓層 f 電梯按鈕只有在第一次被按下時(shí)才會由暗變亮，以后再按它則只會被忽略。在位置 Ff上有令牌，表示在樓層 f
化學(xué)相關(guān)推薦
鄂ICP備17016276號-1