軟體形式規格說明語言

《軟體形式規格說明語言》是2012年由清華大學出版社出版的圖書，作者是繆淮扣。

基本介紹

• 書名：軟體形式規格說明語言
• ISBN：9787302292777
• 頁數：299
• 定價：34.50元
• 出版時間：2012-11
• 副標題：軟體形式規格說明語言Z

內容簡介

《普通高等教育"十一五"國家級規劃教材·軟體工程專業核心課程系列教材:軟體形式規格說明語言(Z)》旨在討論軟體工程中形式方法的概念、方法和表示法，並詳細介紹Z的類型系統、數學語言和公理定義、通用式定義、模式等結構，還討論了z規格說明的推理和求精方法。《普通高等教育"十一五"國家級規劃教材·軟體工程專業核心課程系列教材:軟體形式規格說明語言(Z)》還介紹了面向對象的規格說明語言Object—Z和其他形式方法表示和工具。《普通高等教育"十一五"國家級規劃教材·軟體工程專業核心課程系列教材:軟體形式規格說明語言(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形式規格說明語言Z

1.4.1Z語言概述

1.4.2Z規格說明簡例

小結

習題

第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.1Z的類型系統

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.3Z的基本庫

3.3Z規格說明的構造單元

3.3.1Z的符號

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Δ和Ξ表示

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.4head、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.2Z規格說明的精化原則

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.4Z的精化演算方法

10.5實例研究

10.5.1形式規格說明

10.5.2數據精化

10.5.3轉換為精化演算的抽象程式

10.5.4操作精化

小結

習題

第11章ObjectZ規格說明語言

11.1為何需要面向對象的Z

11.2Object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.10self常量

11.11ObjectZ語言的工具支持

11.12ObjectZ實例研究： 銀行系統

小結

習題

第12章形式方法及其工具

12.1Z規格說明語言支撐工具

12.1.1Z/EVES

12.1.2CADiZ

12.1.3ZTC工具

12.1.4Z User Studio

12.1.5ZeusZ工具

12.1.6Z tools for Word

12.1.7Z規格說明的動畫工具

12.1.8CZT項目

12.1.9其他Z支撐工具

12.2其他形式方法工具

12.2.1PVS

12.2.2Isabelle

12.2.3SPIN

12.2.4SMV

12.2.5Alloy模型分析器

12.3其他形式方法及規格說明語言

12.3.1B方法

12.3.2EventB方法

12.3.3維也納開發方法

12.3.4TCOZ語言

12.3.5LOTOS語言

12.3.6Larch語言

12.3.7通信順序進程

12.3.8時段演算

12.3.9UTP理論

12.3.10SOFL方法

12.3.11TLA+

12.3.12Petri網

小結

習題

附錄AZ語法

附錄BZ語言術語

附錄 CObjectZ語法

C.1表示法

C.2縮寫

C.3產生式

附錄D部分習題解答

參考文獻