軟件形式規格說明語言―Z（簡體書）

《普通高等教育"十一五"國家級規劃教材?軟件工程專業核心課程系列教材:軟件形式規格說明語言(Z)》可作為計算機、軟件工程、信息安全和信息管理等專業本科生和研究生的教材，也可作為大專院校有關專業的教師參考書，還可作為從事軟件工程、軟件開發和軟件應用的研究人員和技術人員的參考資料。

第1章 緒論
1.1 軟件生命周期
1.2 存在的問題
1.3 形式方法
1.3.1 形式化和抽象的需要
1.3.2 什么是形式方法
1.3.3 形式驗證技術
1.3.4 形式方法發展的歷史簡介
1.3.5 形式規格說明語言的分類
1.3.6 形式方法的應用
1.3.7 推薦使用形式方法的相關標準
1.3.8 形式方法的優缺點
1.4 形式規格說明語言2
1.4.1 Z語言概述
1.4.2 2規格說明簡例
小結
習題
第2章 一階邏輯與集合論
2.1 命題邏輯
2.1.1 命題與連接詞
2.1.2 命題公式與真值表
2.2 謂詞邏輯
2.2.1 量詞
2.2.2 謂詞公式
2.2.3 約束變量與自由變量
2.2.4 謂詞公式的解釋
2.3 一階邏輯中的證明
2.3.1 什么是證明
2.3.2 命題邏輯中的證明
2.3.3 命題邏輯中的定律
2.3.4 謂詞邏輯中的證明
2.3.5 謂詞邏輯中的定律
2.4 集合論
2.4.1 集合的表示法
2.4.2 集合謂詞
2.4.3 空集、全集與冪集
2.4.4 集合運算
2.4.5 序偶與笛卡兒積
小結
習題
第3章 Z的類型與構造單元
3.1 Z的類型系統
3.1.1 基本類型
3.1.2 冪集類型
3.1.3 笛卡兒積類型
3.1.4 對象聲明
3.1.5 枚舉類型
3.2 擴充表示法
3.2.1 量詞化擴充表示法
3.2.2 集合表達式擴充表示法
3.2.3 Z的基本庫
3.3 2規格說明的構造單元
3.3.1 Z的符號
3.3.2 公理定義
3.3.3 模式
3.3.4 通用式定義
小結
習題
第4章 關系和函數
4.1 關系
4.1.1 關系表示法
4.1.2 定義域和值域
4.2 關系的運算
4.2.1 關系復合
4.2.2 恒等和閉包
4.2.3 關系的逆
4.2.4 關系限定和限定減
4.2.5 關系映像
4.3 函數
4.3.1 部分函數與全函數
4.3.2 入射函數與滿射函數
4.3.3 函數疊加操作和通用式定義
4.3.4 文具用品管理的模型示例
4.3.5 λ—表示法
小結
習題
第5章 模式和規格說明
5.1 模式的描述功能
5.1.1 模式描述抽象狀態
5.1.2 模式描述操作
5.2 模式的修飾和包含
5.2.1 模式的修飾
5.2.2 模式包含
5.2.3 A和巳表示
5.2.4 初始狀態模式
5.3 模式運算
5.3.1 命題連接詞連接模式
5.3.2 模式復合
5.3.3 一個關于模式復合的例子
5.3.4 前置條件模式
5。4 模式類型和通用模式
5.4。1 模式類型
5.4.2 在聲明中使用模式類型
5.4.3 通用式模式定義
5.5 規格說明文檔的結構
小結
習題
第6章 序列和包
6.1 序列
6.1.1 序列表示和定義
6.1.2 連接和逆置操作
6.1.3 序列應用——一個后備存儲
6.1.4 head、tail、front和last操作
6.1.5 抽取、過濾、壓縮和劃分操作
6.1.6 序列應用二——一個正文編輯的規格說明
6.2 包
6.2.1 包表示、定義和操作函數
6.2.2 一個排序的規格說明
6.2.3 一個自動售貨機的規格說明
小結
習題
第7章 規格說明的實例
7.1 簡介
7.2 存儲分配管理
7.2.1 系統狀態描述
7.2.2 請求分配空閑存儲塊的操作
7.2.3 釋放一個存儲塊的操作
7.2.4 請求分配相鄰的存儲塊集合
7.3 圖書館數據庫管理實例
7.3.1 問題簡介
7.3.2 給定類型和枚舉類型
7.3.3 抽象規格說明
7.4 自由類型的應用——命題邏輯證明器的規格說明
7.4.1 說明一個序列證明
7.4.2 規格說明
小結
習題
第8章 Z規格說明的形式推理
8.1 問題的提出和有關的概念
8.1.1 一個關于“學生興趣小組”的規格說明
8.1.2 規格說明中的定理表示形式
8.1.3 模式作為謂詞
8.2 關于嚴密證明
8.2.1 關于集合的推理
8.2.2 歸納法證明
8.3 一個定律庫
8.4 關于規格說明的推理
8.4.1 引入一個“球迷身份卡”
8.4.2 初始化定理及其證明
8.4.3 前置條件及其簡化
8.4.4 規格說明的性質及其證明
8.4.5 關于精化定理的證明
小結
習題
第9章 Z規格說明的若干推理實例
9.1 兩個初始化定理的證明
9.1.1 存儲管理程序的規格說明中的初始化定理
9.1.2 圖書館數據庫DB的初始化定理
9.2 兩個前置條件的簡化
9.2.1 存儲管理程序中一個前置條件的簡化
9.2.2 正文編輯程序中的一個前置條件的簡化
9.3 規格說明中一般定理的證明
9.3.1 正文編輯程序中的一個定理
9.3.2 圖書館數據庫管理系統中的一個定理
小結
習題
第10章 從規格說明到程序
10.1 程序范疇與軟件精化
10.1.1 程序范疇
10.1.2 軟件精化
10.1.3 崗哨命令語言
10.1.4 精化導向
10.2 2規格說明的精化原則
10.2.1 兩種精化
10.2.2 操作精化
10.2.3 數據精化
10.2.4 數據精化實例
10.2.5 小結
10.3 精化演算
10.3.1 賦值語句
10.3.2 條件語句
10.3.3 邏輯常量
10.3.4 順序復合
10.3.5 循環語句
10.4 Z的精化演算方法
10.5 實例研究
10.5.1 形式規格說明
10.5.2 數據精化
10.5.3 轉換為精化演算的抽象程序
10.5.4 操作精化
小結
習題
第11章 Object—Z規格說明語言
11.1 為何需要面向對象的Z
11.2 Object—Z語言簡介
11.2.1 語法定義
11.2.2 被繼承類
11.2.3 局部定義
11.2.4 狀態模式
11.2.5 初始狀態模式
11.3 操作
11.3.1 操作模式
11.3.2 操作提升
11.3.3 操作運算符
11.3.4 實例說明
11.4 分布運算符
11.5 遞歸定義
11.6 繼承
11.7 對象包含
11.8 多態性
11.9 類合并
11.9.1 定義類合并
11.9.2 多態核心
11.9.3 實例：電動工具
11.9.4 類合并與多態運算符的區別
11.10 self常量
11.11 Object—Z語言的工具支持
11.12 Object—Z實例研究：銀行系統
小結
習題
第12章 形式方法及其工具
12.1 Z規格說明語言支撐工具
12.1.1 2／EVES
12.1.2 CADiZ
12.1.3 ZTC工具
12.1.4 Z User Studio
12.1.5 Zeus—Z工具
12.1.6 Z tools for Word
12.1.7 2規格說明的動畫工具
12.1.8 CZT項目
12.1.9 其他Z支撐工具
12.2 其他形式方法工具
12.2.1 PVS
12.2.2 Isabelle
12.2.3 SPIN
12.2.4 SMV
12.2.5 Alloy模型分析器
12.3 其他形式方法及規格說明語言
12.3.1 B方法
12.3.2 Event—B方法
12.3.3 維也納開發方法
12.3.4 TCOZ語言
12.3.5 LO了OS語言
12.3.6 Larch語言
12.3.7 通信順序進程
12.3.8 時段演算
12.3.9 UTP理論
12.3.10 SOFL方法
12.3.11 TLA+
12.3.12 Petri網
小結
習題
附錄A Z語法
附錄B Z語言術語
附錄C Object—Z語法
C.1 表示法
C.2 縮寫
C.3 產生式
附錄D 部分習題解答
參考文獻

第10章 從規格說明到程序
在過去的若干年中，Z語言被應用于許多軟件系統的規格說明。人們在使用過程中發現：盡管Z規格說明能夠簡明、精確地描述目標軟件系統的結構特征和行為特征，但是軟件開發人員在面對Z規格說明的時候，大多并不清楚如何才能有效地從形式規格說明開發出最終的程序代碼。事實上，Z語言僅是一種規格說明描述語言，并沒有與之相關的程序開發方法，即便是最復雜的Z規格說明，從某種觀點來看也只不過是對目標軟件系統建立的一種數學模型。軟件精化（Software Refinement）是指從抽象規格說明到可執行程序代碼的轉換過程。在精化的過程中可以明確數據是如何存儲的，定義計算是如何實現的，通過逐步消除形式規格說明中的不確定性和非終止性，直到轉化為可執行的程序代碼。本章簡要介紹軟件精化的基本概念和Z規格說明精化的基本原則，討論精化演算理論，并結合一個實例介紹Z規格說明精化的一般方法。
10.1 程序范疇與軟件精化
10.1.1 程序范疇
傳統觀點認為，程序是指導計算機一步一步地執行的指令的有序集合，它由程序設計語言來編寫。傳統觀點中程序可以由計算機直接執行。
程序設計方法學是研究如何編寫程序的科學。本章將介紹從規格說明出發獲得程序的方法。規格說明是對目標軟件系統的功能描述，它由形式規格說明語言來編寫。通常，規格說明不可能交由計算機直接執行，但它較易為人們所理解。因為規格說明是軟件開發人員和用戶之間的一種合約。用戶用規格說明表達他對目標軟件系統的需求，軟件開發人員則依據規格說明開發最終程序代碼。
若放棄傳統觀點中“程序可以由計算機直接執行”的觀點，那么規格說明與程序代碼間的差別就可淡化。在軟件精化中，為了尋求統一的觀點，將規格說明、設計文檔、程序代碼統稱為程序。這樣，程序可以劃分為若干層次：最高層是不能直接執行的程序，即規格說明，它由抽象的描述語句構成；最低層是可以直接執行的程序，稱為程序代碼，它由可執行的命令語句構成，如賦值語句、選擇語句、循環語句及遞歸語句等；最高層和最低層之間的一系列程序稱為混合程序，其中既含有抽象的描述語句，又含有可執行的命令語句（如圖10—1所示）。
由圖中可看出，較之傳統觀點，“程序”一詞的內涵有所增加，從左到右依次為：易理解性較強但可執行性弱的規格說明、一系列描述語句與命令語句并存的混合程序以及易理解性較弱但可執行性強的程序代碼。圖中從左到右，可執行性依次增加，從右到左，易理解性依次加強。