Z形式規約的自動求精研究

《Z形式規約的自動求精研究》敘述簡明清晰，邏輯性強，可作為高等學校相關專業研究生和從事形式語言研究、大型軟件形式化開發與應用的專業人員參考。 Z形式規約是一種世界上廣泛使用的軟件規格說明語言，在軟件開發的需求規格說明階段和軟件設計階段都可以使用，對於提高大型軟件質量、驗證軟件設計正確性等方面具有非常重要的意義。
　　由於Z是以集合論和一階邏輯為基礎，是設計用來給人看的而不能由機器執行。將Z轉換成高級語言需要專業的數學知識，而且對於大型軟件，轉換過程極易出錯。Z的機器可執行性已經引起世界範圍的關注，但目前還不能直接從Z語言自動生成應用程序，Z到可執行代碼的轉換主要由人工完成。《Z形式規約的自動求精研究》指出了Z語言求精方法對於自動生成應用程序的不足，提出了對Z規格說明做一定限制後的Smart Z自動求精為C++和STL方法。

第1章 Z形式規約
1.1 軟件開發的形式化方法
1.2 Z形式規約的類型
1.3 Z形式規約的構造單元
1.4 Z形式規約的關係和函數
1.5 Z形式規約求精技術

第2章 ++標準模板庫STL
2.1 STL簡介
2.2 STL基本結構
2.3 容器
2.4 迭代器
2.5 算法
2.6 其他組件

第3章 Z形式規約的精簡-SmartZ
3.1 概述
3.2 Z形式規約的類型約束
3.3 Z形式規約的謂詞約束
3.4 Z形式規約的精簡

第4章 SmartZ的自動求精
4.1 SmartZ的詞法分析
4.2 SmartZ的語法分析
4.3 SmartZ的語義分析
4.4 SmartZ的自動求精轉換器

第5章 一階邏輯算子的自動求精
5.1 一階邏輯
5.2 一階邏輯算子的自動求精步驟
5.3 表達式處理
5.4 SmartZ的量詞與連接詞的自動求精
5.5 一階邏輯算子的目標代碼生成
5.6 一個模式求精實例

第6章 集合論算子的自動求精
6.1 集合類型的聲明
6.2 目標代碼中的集合操作
6.3 集合論算子到中間代碼的轉換
6.4 採用模板及重載技術設計SmartZ中集合論算子的求精
6.5 集合論算子自動求精實例

第7章 冪集算子的自動求精
7.1 冪集類型
7.2 廣義表
7.3 單層冪集的自動求精
7.4 多層嵌套冪集的自動求精
7.5 冪集的自動求精實例

第8章 笛卡兒積的自動求精
8.1 笛卡兒積的聲明
8.2 笛卡兒積的數據求精
8.3 笛卡兒積的過程求精48
8.4 笛卡兒積的自動求精實例

第9章 關係和函數的自動求精
9.1 序偶與關係
9.2 關係操作與自動求精
9.3 函數操作與自動求精

第10章 序列和包的自動求精
10.1 序列和包
10.2 序列操作的自動求精
10.3 包操作的自動求精
10.4 序列和包的自動求精實例
附錄1 Z語法
附錄2 SmartZ詞法
附錄3 SmartZ的詞法
附錄4 SmartZ語法
附錄5 SmartZ語法的部分SI-NS圖
附錄6 部分SmartZ算子的函數模板
參考文獻