形式化語言課件

1、形式化語言第4章 形式化說明技術(shù)形式化語言形式化方法 所謂形式化方法：是描述系統(tǒng)性質(zhì)的，是基于數(shù)學(xué)的技術(shù)，也就是說，如果一種方法有堅實的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的。形式化語言4.1概述 4.1.1非形式化方法的缺點 用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。 4.1.2形式化方法的優(yōu)點 簡潔準(zhǔn)確描述物理現(xiàn)象、對象或動作的結(jié)果 適合于表示狀態(tài)，表示“做什么” 數(shù)學(xué)規(guī)格說明 可以用數(shù)學(xué)方法驗證形式化語言4.1.3應(yīng)用形式化方法的準(zhǔn)則1 應(yīng)該選用適當(dāng)?shù)谋硎痉椒ǎ糠N形式化語言都有各自的特點）2 應(yīng)該形式化，但不要過分形式化3 應(yīng)該估算成本4 應(yīng)該有

2、形式化方法顧問隨時提供咨詢5 不應(yīng)該放棄傳統(tǒng)的開發(fā)方法6 應(yīng)該建立詳盡的文檔7 不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)8 不應(yīng)該盲目依賴形式化方法9 應(yīng)該測試、測試再測試10 應(yīng)該重用形式化語言4.2有窮狀態(tài)機 4.2.1概念 一個有窮狀態(tài)機包括5部分： J是一個有窮的非空狀態(tài)集； K是一個有窮的非空輸入集 T是一個從（J-F）K到J的轉(zhuǎn)換函數(shù) SJ，是一個初始狀態(tài) FJ，是終態(tài)集形式化語言圖4.1保險箱的狀態(tài)轉(zhuǎn)換圖形式化語言形式化語言保險箱的有窮狀態(tài)機 狀態(tài)集J：保險箱鎖定，A,B，保險箱解鎖，報警 輸入集K：1L,1R,2L,2R,3L,3R 轉(zhuǎn)換函數(shù)T：如表4.1 初始態(tài)S：保險箱鎖定 終態(tài)集F：保險箱解鎖

3、，報警形式化語言4.2.2例子 在一幢M層樓的大廈里，用電梯內(nèi)的和每個樓層的按鈕來控制N部電梯的運動。當(dāng)按下電梯按鈕請求電梯在指定樓層停下時，按鈕指示燈亮；當(dāng)電梯到達(dá)指定樓層時，指示燈滅。除了大廈的最底層和最高層外，每層樓都有兩個按鈕分別指示電梯上行和下行。當(dāng)這兩個按鈕之一被按下時相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時燈熄滅，電梯向要求的方向移動。當(dāng)電梯無升降動作時，關(guān)門并停在當(dāng)前樓層。形式化語言電梯按鈕的狀態(tài)轉(zhuǎn)換圖 EB（e,f）：表示按下電梯e內(nèi)的按鈕，并請求到f層去。有兩個狀態(tài)：-EBON（e,f）：電梯按鈕（e,f）打開-EBOFF（e,f）：電梯按鈕（e,f）關(guān)閉兩個事件：-EBP（e,

4、f）：電梯按鈕（e,f）被按下- EAF（e,f）：電梯e到達(dá)f層形式化語言形式化轉(zhuǎn)換規(guī)則 V（e,f）：電梯e停在f層EBOFF（e,f）+EBP（e,f）+not V（e,f） EBON（e,f）EBON（e,f）+EAF（e,f） EBOFF（e,f）形式化語言樓層按鈕的狀態(tài)轉(zhuǎn)換圖 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（1n,f）：電梯1或或n到達(dá)f層形式化語言形式化轉(zhuǎn)換規(guī)則 S（d，e，f）：電梯e停在f

5、層并且移動方向由d確定為向上（d=U）或向下（d=D）或待定（d=N）。 FBOFF（d,f）+ FBP（d,f）+not S（d，1n，f） FBON（d,f） FBON（d,f）+ EAF（1n,f）+ S（d，1n，f） FBOFF（d,f） 其中d=UorD形式化語言電梯的狀態(tài)轉(zhuǎn)換 電梯的3個狀態(tài)： M（d，e，f）：電梯e沿著d方向移動，即將到達(dá)的是第f層 S（d，e，f）：電梯e停在f層，將朝d方向移動（尚未關(guān)門） W（e，f）：電梯e在f層等待（已關(guān)門） 電梯的3個事件： DC（e，f）：電梯e在樓層f關(guān)上門 ST （e，f）：電梯e靠近f層時觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層

6、電梯是否停下 RL：電梯按鈕或樓層按鈕被按下進(jìn)入打開狀態(tài)形式化語言圖4.4電梯的狀態(tài)轉(zhuǎn)換圖形式化語言形式化轉(zhuǎn)換規(guī)則 S（U，e，f）+DC（e，f） M（U，e，f+1） S（D，e，f）+DC（e，f） M（D，e，f-1） S（N，e，f）+DC（e，f） W（e，f）形式化語言4.3 Petri網(wǎng) 4.3.1概念（描述并發(fā)活動、處理定時需求） 四元組C=（P,T,I,O） P=P1,Pn是一個有窮位置集，n0 T =t1,tm 是一個有窮轉(zhuǎn)換集，m0 I：TP為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射 O：TP 為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射 一個無序單位組或多重組是允許一個

7、元素有多個實例的廣義集形式化語言圖4.5 Petri網(wǎng)的組成圖4.6帶標(biāo)記的Petri網(wǎng)形式化語言圖4.7圖4.6的Petri網(wǎng)在轉(zhuǎn)換t1被激發(fā)后的情況圖4.8圖4.7的Petri網(wǎng)在轉(zhuǎn)換t2被激發(fā)后的情況形式化語言圖4.10 Petri網(wǎng)表示的電梯按鈕形式化語言4.3.2例子1. 電梯按鈕圖4.10 Petri網(wǎng)表示的電梯按鈕形式化語言圖4.11Petri網(wǎng)表示樓層按鈕2. 樓層按鈕形式化語言4.4 Z語言 4.4.1簡介 1. 給定的集合 2. 狀態(tài)定義圖4.12Z格S的格式形式化語言圖4.13Z格Button_State形式化語言3. 初始狀態(tài)4. 操作圖4.14操作Push_Butto

8、n的Z規(guī)格說明形式化語言圖4.15操作Floor_Arrival的Z規(guī)格說明形式化語言將事物的狀態(tài)和行為用數(shù)學(xué)符號形式化表達(dá)的語言，為編寫計算機程序和驗證計算機程序的正確性提供依據(jù)，是軟件工程中編碼之前的規(guī)格說明語言。 Z語言是一種以一階謂詞演算為主要理論基礎(chǔ)的規(guī)約語言,是一種功能性語言。形式化描述語言Z指的是著名數(shù)學(xué)家Zermelo，它是目前使用最廣泛的一種形式化描述語言，在軟件產(chǎn)業(yè)的一些大型項目中已經(jīng)獲得成功的應(yīng)用，Z以帶等詞的一階謂詞邏輯ZF（Zermelo-Fraenkel，蔡梅羅-弗蘭科爾）公理集合論為主要數(shù)學(xué)基礎(chǔ)。在Z中有兩種語言：數(shù)學(xué)語言和模式（Schema）語言。數(shù)學(xué)語言用來描述系統(tǒng)的各種特征：對象及其之間的關(guān)系。模式語言是一種半圖形化的語言，它用來構(gòu)造、組織形式化說明的描述、整理、封裝信息塊并對其命名以便可以重用這些信息塊。通常，形式化說明的可讀性都不太好，但由于Z采用半圖形化的模式語言，能用一種比較直觀、有條理的方式來表達(dá)形式化說明，這就改善了可讀性。Z語言是由牛津大學(xué)程序設(shè)計研究小組開發(fā)的一種形式語言，之后該小組與IBM的Hursley實驗室合作，將Z