第六講軟件工程的形式化說(shuō)明技術(shù)軟件工程使用的描述技術(shù)有三類：非形式化技術(shù)、半形式化技術(shù)和形式化技術(shù)。所謂非形式化技術(shù)的代表方法是用自然語(yǔ)言描述的需求規(guī)格說(shuō)明；所謂半形式化技術(shù)的代表方法有數(shù)據(jù)流圖、E-R圖和UML等；所謂形式化技術(shù)的方法有很多，其中具有代表性的方法包括有：時(shí)序邏輯語(yǔ)言、有窮狀態(tài)機(jī)、Petri網(wǎng)系統(tǒng)和Z語(yǔ)言等；所謂形式化規(guī)格說(shuō)明語(yǔ)言的關(guān)鍵思想是把軟件開發(fā)過(guò)程中的需求規(guī)格說(shuō)明階段和軟件設(shè)計(jì)說(shuō)明階段分開，在需求規(guī)格說(shuō)明階段精確地描述軟件“做什么”，而不涉及“怎么做”。編寫規(guī)格說(shuō)明與編寫計(jì)算機(jī)程序的不同之處在于規(guī)格說(shuō)明是對(duì)目標(biāo)軟件系統(tǒng)的功能描述，而計(jì)算機(jī)系統(tǒng)則是實(shí)現(xiàn)目標(biāo)軟件系統(tǒng)功能的過(guò)程描述。形式化和非形式化描述方法各有優(yōu)缺點(diǎn)形式化描述的優(yōu)點(diǎn)：使用形式化方法可以嚴(yán)格準(zhǔn)確地描述出系統(tǒng)對(duì)象；使用形式化方法描述的系統(tǒng)可以向任意具體系統(tǒng)進(jìn)行映射轉(zhuǎn)換；可以對(duì)形式化描述的系統(tǒng)進(jìn)行嚴(yán)格的數(shù)學(xué)證明分析；形式化描述的缺點(diǎn)：形式化描述方法難以使用；使用形式化描述一個(gè)龐大的實(shí)際系統(tǒng)存在許多困難，在實(shí)際應(yīng)用中有許多問(wèn)題本身就是模糊或非確定的無(wú)法使用嚴(yán)格的形式化方法進(jìn)行描述；3.形式化描述的模型對(duì)于那些沒(méi)有經(jīng)過(guò)專門的訓(xùn)練用戶來(lái)說(shuō)很難理解；形式化說(shuō)明的正確性證明費(fèi)時(shí)費(fèi)力；尚未出現(xiàn)支持形式化風(fēng)格全過(guò)程的軟件環(huán)境；非形式化方法的優(yōu)點(diǎn)：描述的模型直觀，容易理解；非形式的描述技術(shù)比較簡(jiǎn)單，容易學(xué)習(xí)；許多的應(yīng)用只能使用非形式化的方法描述；非形式化方法的缺點(diǎn)：非形式化的描述可能存在矛盾、二意性和含糊性等問(wèn)題；難以進(jìn)行嚴(yán)格的證明工作；對(duì)于高可靠性的系統(tǒng)，使用該方法描述存在潛在的問(wèn)題；本文介紹三種形式化方法：有窮狀態(tài)機(jī)、Petri網(wǎng)、Z語(yǔ)言有窮狀態(tài)機(jī)：使用一個(gè)六元組來(lái)準(zhǔn)確地描述系統(tǒng)狀態(tài)的變化的一種形式化方法。當(dāng)前狀態(tài)+事件+謂詞=＞下一個(gè)狀態(tài)Petri網(wǎng)：Petri的背景：Petri網(wǎng)的首次提出是由德國(guó)科學(xué)家Petri于1962年在他的博士論文《用自動(dòng)機(jī)通訊》中提出的使用網(wǎng)狀結(jié)構(gòu)模擬通訊系統(tǒng)。Petri網(wǎng)有時(shí)又被稱為網(wǎng)論。Petri的知識(shí)結(jié)構(gòu)包括有基本網(wǎng)系統(tǒng)為主的特殊網(wǎng)論和通用網(wǎng)論。Petri網(wǎng)的本質(zhì)是：將系統(tǒng)的動(dòng)態(tài)行為表現(xiàn)為資源的流動(dòng)。程序系統(tǒng)的動(dòng)態(tài)特性分為兩類：安全性和進(jìn)展性。安全性要求所有可能的狀態(tài)均具有一定的性質(zhì)，并要求變化服從給定的規(guī)律，其關(guān)心的是可能性；進(jìn)展性要求某些特定的狀態(tài)一定能夠達(dá)到的，其關(guān)心的是必然性；有時(shí)人們也提到描述系統(tǒng)性質(zhì)的活性，其等同于進(jìn)展性；基本網(wǎng)論（EN_系統(tǒng)）基本網(wǎng)系統(tǒng)中的狀態(tài)元素被稱為條件，變遷元素被稱為事件。事件的發(fā)生改變條件的狀態(tài)，引起信息在網(wǎng)上的流動(dòng)。條件/事件系統(tǒng)（C/E_系統(tǒng)）非形式地說(shuō)，滿足一定要求的基本網(wǎng)系統(tǒng)就是一個(gè)C/E—系統(tǒng)；為簡(jiǎn)單網(wǎng)；每個(gè)條件都有機(jī)會(huì)成真，也有機(jī)會(huì)成假；每個(gè)事件都有機(jī)會(huì)發(fā)生；C/E—系統(tǒng)是通用網(wǎng)論的基礎(chǔ)。基本網(wǎng)論和條件/事件網(wǎng)論是構(gòu)成其他各級(jí)網(wǎng)系統(tǒng)的基礎(chǔ)，C/E—系統(tǒng)是通用網(wǎng)論的基礎(chǔ)。庫(kù)所/變遷系統(tǒng)（P/T_系統(tǒng)）P表示庫(kù)所，T代表變遷，該系統(tǒng)是最早期的Petri網(wǎng)的形式，主要以研究資源流動(dòng)為特征。是以孤立的網(wǎng)系統(tǒng)為對(duì)象，以尋求分析技術(shù)和應(yīng)用方法為目標(biāo)的“特殊”網(wǎng)系統(tǒng)。P_元被稱為庫(kù)所（place）；T_元被稱為變遷；P_元中的黑點(diǎn)個(gè)數(shù)被稱為資源的數(shù)量，每個(gè)黑點(diǎn)被稱為托肯（token）又被稱為標(biāo)記和令牌；帶箭頭的連線表示資源流動(dòng)的方向；箭頭上的數(shù)字表示組裝所需或產(chǎn)生該種資源的數(shù)量，稱為弧上的權(quán)；K表示庫(kù)所的容量；

實(shí)例一：火車調(diào)度系統(tǒng)設(shè)計(jì)實(shí)例二：處理兩個(gè)進(jìn)程的同步問(wèn)題進(jìn)程得到資源占用資源運(yùn)行釋放資源不使用資源運(yùn)行PR1廠LOCKR—處理11tUNLOCKR—處理12—PR2廠LOCKR—處理21—UNLOCKR—處理22—j實(shí)例三：生產(chǎn)流水線系統(tǒng)（來(lái)分析什么是沖突、餓死和死鎖）通用網(wǎng)論P(yáng)etri網(wǎng)的通用網(wǎng)論主要研究?jī)?nèi)容是：以網(wǎng)系統(tǒng)的全體作為研究對(duì)象，研究其分類及各分類之間的關(guān)系，發(fā)展了以并發(fā)論，同步論和網(wǎng)邏輯、網(wǎng)拓?fù)浜托畔⒘鹘Y(jié)構(gòu)為主要研究?jī)?nèi)容的理論體系。網(wǎng)邏輯（enlogy）:是以推論為基礎(chǔ)的直觀語(yǔ)義框架。研究的系統(tǒng)中不能夠發(fā)生的事件與系統(tǒng)行為的關(guān)系。這些事件是由于一完備化操作構(gòu)造而得的。同步論：為各種同步現(xiàn)象（發(fā)送、傳遞和接收信息的這些動(dòng)作之間的同步）提供定量的描述，與網(wǎng)邏輯結(jié)合使用是一種有效的系統(tǒng)規(guī)范設(shè)計(jì)工具。信息流結(jié)構(gòu)：通俗地說(shuō)就是信息流圖的網(wǎng)表示，是溝通網(wǎng)論和其他學(xué)科的界面網(wǎng)拓?fù)洌╪ettopology）:空間的拓?fù)浣Y(jié)構(gòu)是區(qū)分離散數(shù)學(xué)和連續(xù)數(shù)學(xué)的基礎(chǔ)。拓?fù)淇臻g的連續(xù)映射既是連續(xù)數(shù)學(xué)的主要研究工具，同時(shí)又是連續(xù)數(shù)學(xué)的主要研究對(duì)象。由于實(shí)際應(yīng)用中的網(wǎng)系統(tǒng)一般都只有有限多個(gè)節(jié)點(diǎn)，在通常的拓?fù)湟饬x下不可能連續(xù)的。必須有適用于網(wǎng)系統(tǒng)拓?fù)洌淳W(wǎng)拓?fù)洹２l(fā)論：如果ab和ba的后果是一樣的，a和b就并行，或a與b并行則ab和ba效果一樣。Z語(yǔ)言：背景Z語(yǔ)言是70年代末至80年代初由英國(guó)Oxford大學(xué)研究組PRG的JeanRaym