軟件工程PART12024/5/162第四章形式化說明技術(shù)CONTENTS放棄美麗的女人讓人心碎。自然語言：矛盾、二義性、含糊形式化表示：準確、清晰非形式化：自然語言半形式化：DFD、E-R圖形式化：堅實的以數(shù)學(xué)為基礎(chǔ)的表示方法0102第四章形式化說明技術(shù)概述有窮狀態(tài)機Petri網(wǎng)Z語言概述有窮狀態(tài)機Petri網(wǎng)Z語言4.1概述2024/5/164.1.1非形式化方法的缺點矛盾：相互沖突的陳述二義性：讀者可以用不同的方式理解的陳述含糊不完整抽象層次混亂：非常抽象的陳述中混進了一些關(guān)于細節(jié)的低層次陳述。#202244.1概述2024/5/164.1.2形式化方法的優(yōu)點把數(shù)學(xué)引入軟件開發(fā)過程，形成基于數(shù)學(xué)的形式化方法。數(shù)學(xué)最有用的一個性質(zhì)是，能夠簡潔準確地描述物理現(xiàn)象、對象或動作的結(jié)果，因此是理想的建模工具。在軟件開發(fā)過程中使用數(shù)學(xué)，可以在不同的軟件工程活動之間平滑地過渡。提供了高層確認的手段。#202254.1概述2024/5/164.1.3應(yīng)用形式化方法的準則應(yīng)該選用適當(dāng)?shù)谋硎痉椒☉?yīng)該形式化，但不要過分形式化應(yīng)該估算成本應(yīng)該有形式化方法顧問隨時提供咨詢不應(yīng)該放棄傳統(tǒng)的開發(fā)方法應(yīng)該建立詳盡的文檔不應(yīng)該放棄質(zhì)量標準不應(yīng)該盲目依賴形式化方法應(yīng)該測試、測試再測試應(yīng)該重用#20226有窮狀態(tài)機概念一個保險箱上裝了一個復(fù)合鎖，鎖有3個位置，分別標記為1、2、3，轉(zhuǎn)盤可向左（L）或向右（R）轉(zhuǎn)動。這樣，任何時刻轉(zhuǎn)盤都有6種可能的運動，即1L、1R、2L、2R、3L、3R。保險箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤的任何其他運動都將引起報警。4.2有窮狀態(tài)機2024/5/168圖4.1保險箱的狀態(tài)轉(zhuǎn)換圖4.2有窮狀態(tài)機2024/5/1694.2有窮狀態(tài)機一個有窮狀態(tài)機包括5個部分：狀態(tài)集J：{保險箱鎖定，A，B，保險箱解鎖， 報警}輸入集K：{1L、1R、2L、2R、3L、3R}轉(zhuǎn)換函數(shù)T：如表4.1所示初始態(tài)S：保險箱鎖定終態(tài)集F：{保險箱解鎖，報警}#2022104.2有窮狀態(tài)機2024/5/16一個有窮狀態(tài)機可以表示為一個5元組（J，K，T，S，F(xiàn)），其中：J是一個有窮的非空狀態(tài)集；K是一個有窮的非空輸入集；T是一個從（J-F）*K到J的轉(zhuǎn)換函數(shù)；S∈J，是一個初始狀態(tài)；FJ，是終態(tài)集一個有窮狀態(tài)機可以表示為一個5元組（J，K，T，S，F(xiàn)），其中：J是一個有窮的非空狀態(tài)集；K是一個有窮的非空輸入集；T是一個從（J-F）*K到J的轉(zhuǎn)換函數(shù)；S∈J，是一個初始狀態(tài)；FJ，是終態(tài)集114.2有窮狀態(tài)機2024/5/1612加入謂詞集P，把有窮狀態(tài)機擴展為一個6元組，其中每個謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。01則轉(zhuǎn)換函數(shù)T：（J-F）*K*PJ024.2有窮狀態(tài)機4.2.2例子電梯按鈕EB（e，f）：按下電梯e內(nèi)的按鈕并請求到f層去狀態(tài)：EBON（e，f）：電梯按鈕（e，f）打開EBOFF（e，f）：電梯按鈕（e，f）關(guān)閉事件EBP（e，f）：電梯按鈕（e，f）被按下EAF（e，f）：電梯到達f層謂詞V（e，f）：電梯e停在f層134.2有窮狀態(tài)機2024/5/1614圖4.2電梯按鈕的狀態(tài)轉(zhuǎn)換圖4.2有窮狀態(tài)機15樓層按鈕FB（d，f）：f層請求電梯向d方向運動的按鈕狀態(tài)：FBON（d，f）：樓層按鈕（d，f）打開FBOFF（d，f）：樓層按鈕（d，f）關(guān)閉事件FBP（d，f）：樓層按鈕（d，f）被按下EAF（1…n，f）：電梯1或…或n到達f層謂詞S（d，e，f）：電梯e停在f層并且移動方向由d確定#20224.2有窮狀態(tài)機2024/5/1616圖4.3樓層按鈕的狀態(tài)轉(zhuǎn)換圖4.2有窮狀態(tài)機電梯狀態(tài)M（d，e，f）：電梯e正沿d方向移動，即將到達的是第f層S（d，e，f）：電梯e停在f層，將朝d方向移動（尚未關(guān)門）W（e，f）：電梯e在f層等待（已關(guān)門）事件DC（e，f）：電梯e在樓層f關(guān)上門ST（e，f）：電梯e靠近f層時觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下RL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求4.2有窮狀態(tài)機2024/5/1618圖4.4電梯的狀態(tài)轉(zhuǎn)換圖4.2有窮狀態(tài)機2024/5/1619關(guān)門之時的規(guī)則思考題2024/5/1620231從等待到移動，如何表示O（e，f）：電梯e在f層開門，則如何進入這個狀態(tài)定義狀態(tài)：4.2有窮狀態(tài)機#20224.2.3評價有窮狀態(tài)機描述規(guī)格說明：當(dāng)前狀態(tài)+事件+謂詞下個狀態(tài)優(yōu)點：易于書寫、易于驗證、精確、易于理解缺點：開發(fā)大系統(tǒng)時三元組的數(shù)量會迅速增長沒有處理定時的需求4.3Petri網(wǎng)2024/5/1622概述并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題同步問題競爭條件死鎖Petri網(wǎng)是一種用于確定系統(tǒng)中隱含的定時問題的一種有效技術(shù)可有效的描述并發(fā)活動4.3Petri網(wǎng)2024/5/1623單擊此處添加正文，文字是您思想的提煉，為了演示發(fā)布的良好效果，請言簡意賅地闡述您的觀點。包含元素01{P1，P2，P3，P4}位置P：02{t1，t2}轉(zhuǎn)換T：03I（t1）={P2，P4}I（t2）={P2}輸入函數(shù)I：04O（t1）={P1}O（t2）={P3，P3}輸出函數(shù)O05圖4.5Petri網(wǎng)的組成4.3Petri網(wǎng)更形式化的Petri網(wǎng)結(jié)構(gòu)，是一個四元組C=（P，T，I，O）其中，P={P1，…，Pn}是一個有窮位置集，n>=0T={t1，…，tm}是一個有窮轉(zhuǎn)換集，m>=0，且T和P不相交。I：為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。O：為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。24Petri網(wǎng)Petri網(wǎng)的標記是在Petri網(wǎng)中權(quán)標(token)的分配。圖4.6帶標記的Petri網(wǎng)（1，2，0，1）圖4.7圖4.6的Petri網(wǎng)在轉(zhuǎn)換t1被激發(fā)后的情況（2，1，0，0）圖4.8圖4.7的Petri網(wǎng)在轉(zhuǎn)換t2被激發(fā)后的情況（2，0，2，0）4.3Petri網(wǎng)2024/5/1626對Petri網(wǎng)的一個重要擴充是加入禁止線。禁止線是用一個小圓圈而不是用箭頭標記的輸入線。通常，當(dāng)每個輸入線上至少有一個令牌，而禁止線上沒有令牌的時候，相應(yīng)的轉(zhuǎn)換才是允許的。1圖4.9含禁止線的Petri網(wǎng)24.3Petri網(wǎng)014.3.2例子02每個樓層用一個位置Ff代表(1≤f≤m)03電梯是用一個權(quán)標代表。04在位置Ff上有權(quán)標，表示在樓層f上有電梯。27Petri網(wǎng)電梯按鈕電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示(1≤f≤m)。在EBf上有一個令牌，就表示電梯內(nèi)樓層f的按鈕被按下了。電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示(1≤f≤m)。在EBf上有一個令牌，就表示電梯內(nèi)樓層f的按鈕被按下了。4.3Petri網(wǎng)2024/5/1629樓層按鈕在Petri網(wǎng)中樓層按鈕用位置和表示，分別代表f樓層請求電梯上行和下行的按鈕。4.4Z語言#20224.4.1簡介用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4個部分。給定的集合、數(shù)據(jù)類型及常數(shù)。狀態(tài)定義。初始狀態(tài)。操作。4.4Z語言2024/5/1631從一系列給定的初始化集合開始。即不需要詳細定義的集合，這種集合用帶方括號的形式表示。〔Button〕給定的集合從一系列給定的初始化集合開始。即不需要詳細定義的集合，這種集合用帶方括號的形式表示?！睟utton〕Z語言狀態(tài)定義一個Z規(guī)格說明由若干個“格(schema)”組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。4.4Z語言2024/5/1633單擊此處添加正文，文字是您思想的提煉，為了演示發(fā)布的良好效果，請言簡意賅地闡述您的觀點。您的內(nèi)容已經(jīng)簡明扼要，字字珠璣，但信息卻千絲萬縷、錯綜復(fù)雜，需要用更多的文字來表述；但請您盡可能提煉思想的精髓，否則容易造成觀者的閱讀壓力，適得其反。正如我們都希望改變世界，希望給別人帶去光明，但更多時候我們只需要播下一顆種子，自然有微風(fēng)吹拂，雨露滋養(yǎng)。恰如其分地表達觀點，往往事半功倍。當(dāng)您的內(nèi)容到達這個限度時，或許已經(jīng)不純粹作用于演示，極大可能運用于閱讀領(lǐng)域；無論是傳播觀點、知識分享還是匯報工作，內(nèi)容的詳盡固然重要，但請一定注意信息框架的清晰，這樣才能使內(nèi)容層次分明，頁面簡潔易讀。如果您的內(nèi)容確實非常重要又難以精簡，也請使用分段處理，對內(nèi)容進行簡單的梳理和提煉，這樣會使邏輯框架相對清晰。1圖4.13描述了格Button_State符號P表示冪集(即給定集的所有子集)。約束條件聲明，floor_buttons集與elevator_buttons集不相交，而且它們共同組成buttons集2單擊此處添加正文，文字是您思想的提煉，為了演示發(fā)布的良好效果，請言簡意賅地闡述您的觀點。您的內(nèi)容已經(jīng)簡明扼要，字字珠璣，但信息卻千絲萬縷、錯綜復(fù)雜，需要用更多的文字來表述；但請您盡可能提煉思想的精髓，否則容易造成觀者的閱讀壓力，適得其反。正如我們都希望改變世界，希望給別人帶去光明，但更多時候我們只需要播下一顆種子，自然有微風(fēng)吹拂，雨露滋養(yǎng)。恰如其分地表達觀點，往往事半功倍。當(dāng)您的內(nèi)容到達這個限度時，或許已經(jīng)不純粹作用于演示，極大可能運用于閱讀領(lǐng)域；無論是傳播觀點、知識分享還是匯報工作，內(nèi)容的詳盡固然重要，但請一定注意信息框架的清晰，這樣才能使內(nèi)容層次分明，頁面簡潔易讀。如果您的內(nèi)容確實非常重要又難以精簡，也請使用分段處理，對內(nèi)容進行簡單的梳理和提煉，這樣會使邏輯框架相對清晰。3圖4.13Z格Button_State44.4Z語言2024/5/1634抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。Button_Init〔Button_State｜pushed=〕01初始狀態(tài)02如果一個原來處于關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。03操作04Z語言假設(shè)電梯到達了某樓層，如果相應(yīng)的樓層按鈕已經(jīng)打開，則此時它會關(guān)閉；同樣，如果相應(yīng)的電梯按鈕已經(jīng)打開，則此時它也會關(guān)閉。4.4Z語言#20224.4.2評價Z作為應(yīng)用得最廣泛的形式化語言，在大型項目中的優(yōu)勢更加明顯。Z語言之所以會獲得如此多的成功，主要有以下幾個原因：（1）可以比較容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯誤；（2）用Z寫規(guī)格說明時，要求作者十分精確地使用Z說明符。單擊此處添加正文，文字是您思想的提煉，為了演示發(fā)布的良好效果，請言簡意賅地闡述您的觀點。您的內(nèi)容已經(jīng)簡明扼要，字字珠璣，但信息卻千絲萬縷、錯綜復(fù)雜，需要用更多的文字來表述；但請您盡可能提煉思想的精髓，否則容易造成觀者的閱讀壓力，適得其反。正如我們都希望改變世界，希望給別人帶去光明，但更多時候我們只需要播下一顆種子，自然有微風(fēng)吹拂，雨露滋養(yǎng)。恰如其分地表達觀點，往往事半功倍。當(dāng)您的內(nèi)容到達這個限度時，或許已經(jīng)不純粹作用于演示，極大可能運用于閱讀領(lǐng)域；無論是傳播觀點、知識分享還是匯報工作，內(nèi)容的詳盡固然重要，但請一定注意信息框架的清晰，這樣才能使內(nèi)容層次分明，頁面簡潔易讀。如果您的內(nèi)容確實非常重要又難以精簡，也請使用分段處理，對內(nèi)容進行簡單的梳理和提煉，這樣會使邏輯框架相對清晰。為了能讓您有更直觀的字數(shù)感受，并進一步方便使用，我們設(shè)置了文本的最大限度，當(dāng)您輸入的文字到這里時，已瀕臨頁面容納內(nèi)容的上限，若還有更多內(nèi)容，請酌情縮小字號，但我們不建議您的文本字號小于14磅，請您務(wù)必注意。單擊此處添加正文，Z是一種形式化語言，在需要時開發(fā)者可以嚴格地驗證規(guī)格說明的正確性。雖然完全學(xué)會Z語言相當(dāng)困難，但是，經(jīng)驗表明，只學(xué)過中學(xué)數(shù)學(xué)的軟件開發(fā)人員仍然可以