第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部分习题解答

参考文献