第4章　形式化說明技術

4.1　復習筆記

一、概述

1非形式化方法的缺點

（1）矛盾；

（2）二義性；

（3）含糊性；

（4）不完整性；

（5）抽象層次混亂。

【注意】用自然語言描述需求規格說明，是典型的非形式化方法。

2形式化方法的優點

（1）能保證規格說明中盡可能沒有矛盾、二義性、含糊性和不完整性。

（2）可以在不同的軟件工程活動之間平滑地過渡。

（3）提供了高層確認的手段。

3形式化方法的缺點

（1）難于表示問題的時序、控制和行為等方面的需求。

（2）相比欠形式化方法，它更難學習，培訓的投資過大。

【注意】如果一種方法有堅實的數學基礎，那么它就是形式化的。

4應用形式化方法的準則

（1）應該選用適當的表示方法。

（2）應該形式化，但不要過分形式化。

（3）應該估算成本。

（4）應該有形式化方法顧問隨時提供咨詢。

（5）不應該放棄傳統的開發方法。

（6）應該建立詳盡的文檔。

（7）不應該放棄質量標準。

（8）不應該盲目依賴形式化方法。

（9）應該測試、測試再測試。

（10）應該重用。

二、有窮狀態機

1概念

（1）定義

有窮狀態機是表達規格說明的一種形式化方法。

（2）構成

一個有窮狀態機包括下述5個部分：狀態集J、輸入集K、由當前狀態和當前輸入確定下一個狀態（次態）的轉換函數T、初始態S和終態集F。一個有窮狀態機可以表示為一個5元組（J，K，T，S，F）。其中：J是一個有窮的非空狀態集；K是一個有窮的非空輸入集；T是一個從(J-F)×K到J的轉換函數；S∈J，是一個初始狀態；F?J，是終態集。

（3）狀態轉換形式

當前狀態[菜單]＋事件[所選擇的項]?下個狀態

（4）謂詞集P

①謂詞集P把有窮狀態機擴展為一個6元組，其中每個謂詞都是系統全局狀態Y的函數。

②加入謂詞集后轉換規則形式為：當前狀態[菜單]＋事件[所選擇的項]＋謂詞?下個狀態。

2評價

（1）優點

①采用易于書寫、易于驗證的格式來描述規格說明，能容易地把規格說明轉變成設計或程序代碼。

②比數據流圖技術更精確且易于理解。

（2）缺點

①在開發一個大系統時，三元組（即狀態、事件、謂詞）的數量會迅速增長。

②形式化的有窮狀態機方法沒有處理定時需求。

三、Petri網

1概念

（1）構成

①一般構成

Petri網包含4種元素：一組位置P、一組轉換T、輸入函數I，以及輸出函數O。如圖4-1為Petri網的實例。

圖4-1　Petri網的組成

a．一組位置P為{P₁，P₂，P₃，P₄}，在圖中用圓圈代表位置。

b．一組轉換T為{T₁，T₂}，在圖中用短直線表示轉換。

c．兩個用于轉換的輸入函數，用由位置指向轉換的箭頭表示，它們是：

I(t₁)={P₂，P₄}

I(t₂)={P₂}

d．兩個用于轉換的輸出函數，用由轉換指向位置的箭頭表示，它們是：

O(t₁)={P₁}

O(t₂)={P₃，P₃}

【注意】輸出函數O(t₁)中有兩個P₃，是因為有兩個箭頭由t₂指向P₃。

②形式化的Petri網

更形式化的Petri網結構是一個四元組：

C=(P，T，I，O)

其中：

a．P={P₁，…，P_n}是一個有窮位置集，n≥0。

b．T={t₁，…，t_m}是一個有窮轉換集，m≥0，且T和P不相交。

c．I：T→P^∞為輸入函數，是由轉換到位置無序單位組（bags）的映射。

d．O：T→P^∞為輸出函數，是由轉換到位置無序單位組的映射。

（2）作用

用于確定系統中隱含的定時問題，可以有效地描述并發活動。

四、Z語言

1組成部分

（1）給定的集合；

（2）狀態定義；

（3）初始狀態；

（4）操作。

2優點

（1）可以比較容易地發現用Z寫的規格說明的錯誤；

（2）使用Z寫規格說明時對精確性要求高，減少了模糊性、不一致性和遺漏；

（3）可以降低軟件開發費用；

（4）用Z寫規格說明，更加清楚和正確。