第1章 绪论 1
1.1软件生命周期 2
1.2存在的问题 4
1.3形式方法 4
1.3.1形式化和抽象的需要 4
1.3.2什么是形式方法 5
1.3.3形式验证技术 5
1.3.4形式方法发展的历史简介 6
1.3.5形式规格说明语言的分类 6
1.3.6形式方法的应用 7
1.3.7推荐使用形式方法的相关标准 7
1.3.8形式方法的优缺点 8
1.4形式规格说明语言Z 9
1.4.1 Z语言概述 9
1.4.2 Z规格说明简例 9
小结 10
习题 11
第2章 一阶逻辑与集合论 12
2.1命题逻辑 12
2.1.1命题与连接词 12
2.1.2命题公式与真值表 14
2.2谓词逻辑 14
2.2.1量词 15
2.2.2谓词公式 15
2.2.3约束变量与自由变量 15
2.2.4谓词公式的解释 16
2.3一阶逻辑中的证明 16
2.3.1什么是证明 17
2.3.2命题逻辑中的证明 17
2.3.3命题逻辑中的定律 19
2.3.4谓词逻辑中的证明 22
2.3.5谓词逻辑中的定律 22
2.4集合论 26
2.4.1集合的表示法 26
2.4.2集合谓词 26
2.4.3空集、全集与幂集 27
2.4.4集合运算 27
2.4.5序偶与笛卡儿积 29
小结 30
习题 30
第3章Z的类型与构造单元 31
3.1 Z的类型系统 31
3.1.1基本类型 31
3.1.2幂集类型 32
3.1.3笛卡儿积类型 33
3.1.4对象声明 34
3.1.5枚举类型 35
3.2扩充表示法 36
3.2.1量词化扩充表示法 36
3.2.2集合表达式扩充表示法 37
3.2.3 Z的基本库 38
3.3 Z规格说明的构造单元 39
3.3.1 Z的符号 39
3.3.2公理定义 40
3.3.3模式 41
3.3.4通用式定义 42
小结 44
习题 44
第4章 关系和函数 48
4.1关系 48
4.1.1关系表示法 49
4.1.2定义域和值域 50
4.2关系的运算 51
4.2.1关系复合 52
4.2.2恒等和闭包 53
4.2.3关系的逆 55
4.2.4关系限定和限定减 56
4.2.5关系映像 58
4.3函数 59
4.3.1部分函数与全函数 60
4.3.2入射函数与满射函数 61
4.3.3函数叠加操作和通用式定义 64
4.3.4文具用品管理的模型示例 66
4.3.5 λ-表示法 68
小结 68
习题 69
第5章 模式和规格说明 74
5.l模式的描述功能 74
5.1.1模式描述抽象状态 74
5.1.2模式描述操作 75
5.2模式的修饰和包含 76
5.2.1模式的修饰 76
5.2.2模式包含 77
5.2.3Δ和？表示 78
5.2.4初始状态模式 80
5.3模式运算 81
5.3.1命题连接词连接模式 81
5.3.2模式复合 84
5.3.3一个关于模式复合的例子 86
5.3.4前置条件模式 89
5.4模式类型和通用模式 90
5.4.1模式类型 90
5.4.2在声明中使用模式类型 91
5.4.3通用式模式定义 92
5.5规格说明文档的结构 93
小结 95
习题 96
第6章 序列和包 98
6.1序列 98
6.1.1序列表示和定义 98
6.1.2连接和逆置操作 100
6.1.3序列应用一——一个后备存储 103
6.1.4 head、tail、front和last操作 104
6.1.5抽取、过滤、压缩和划分操作 106
6.1.6序列应用二——一个正文编辑的规格说明 108
6.2包 114
6.2.1包表示、定义和操作函数 114
6.2.2一个排序的规格说明 117
6.2.3一个自动售货机的规格说明 118
小结 124
习题 124
第7章 规格说明的实例 128
7.1简介 128
7.2存储分配管理 129
7.2.1系统状态描述 129
7.2.2请求分配空闲存储块的操作 130
7.2.3释放一个存储块的操作 132
7.2.4请求分配相邻的存储块集合 134
7.3图书馆数据库管理实例 136
7.3.1问题简介 136
7.3.2给定类型和枚举类型 136
7.3.3抽象规格说明 137
7.4自由类型的应用——命题逻辑证明器的规格说明 148
7.4.1说明一个序列证明 148
7.4.2规格说明 150
小结 151
习题 151
第8章 Z规格说明的形式推理 155
8.1问题的提出和有关的概念 155
8.1.1一个关于“学生兴趣小组”的规格说明 155
8.1.2规格说明中的定理表示形式 158
8.1.3模式作为谓词 158
8.2关于严密证明 159
8.2.1关于集合的推理 159
8.2.2归纳法证明 162
8.3一个定律库 164
8.4关于规格说明的推理 167
8.4.1引入一个“球迷身份卡” 168
8.4.2初始化定理及其证明 168
8.4.3前置条件及其简化 170
8.4.4规格说明的性质及其证明 173
8.4.5关于精化定理的证明 177
小结 177
习题 177
第9章Z规格说明的若干推理实例 179
9.1两个初始化定理的证明 179
9.1.1存储管理程序的规格说明中的初始化定理 179
9.1.2图书馆数据库DB的初始化定理 179
9.2两个前置条件的简化 181
9.2.1存储管理程序中一个前置条件的简化 181
9.2.2正文编辑程序中的一个前置条件的简化 182
9.3规格说明中一般定理的证明 183
9.3.1正文编辑程序中的一个定理 183
9.3.2图书馆数据库管理系统中的一个定理 185
小结 185
习题 186
第10章 从规格说明到程序 187
10.1程序范畴与软件精化 187
10.1.1程序范畴 187
10.1.2软件精化 188
10.1.3岗哨命令语言 188
10.1.4精化导向 189
10.2 Z规格说明的精化原则 190
10.2.1两种精化 190
10.2.2操作精化 190
10.2.3数据精化 192
10.2.4数据精化实例 194
10.2.5小结 197
10.3精化演算 198
10.3.1赋值语句 199
10.3.2条件语句 201
10.3.3逻辑常量 202
10.3.4顺序复合 202
10.3.5循环语句 203
10.4 Z的精化演算方法 204
10.5实例研究 207
10.5.1形式规格说明 207
10.5.2数据精化 208
10.5.3转换为精化演算的抽象程序 210
10.5.4操作精化 211
小结 212
习题 213
第11章Object-Z规格说明语言 215
11.1为何需要面向对象的Z 215
11.2 Object-Z语言简介 217
11.2.1语法定义 217
11.2.2被继承类 219
11.2.3局部定义 219
11.2.4状态模式 219
11.2.5初始状态模式 220
11.3操作 221
11.3.1操作模式 221
11.3.2操作提升 223
11.3.3操作运算符 223
11.3.4实例说明 225
11.4分布运算符 226
11.5递归定义 227
11.6继承 228
11.7对象包含 230
11.8多态性 231
11.9类合并 232
11.9.1定义类合并 233
11.9.2多态核心 233
11.9.3实例：电动工具 233
11.9.4类合并与多态运算符的区别 235
11.10 self常量 235
11.11 Obj ect-Z语言的工具支持 236
11.12 Object-Z实例研究：银行系统 237
小结 238
习题 238
第12章 形式方法及其工具 240
12.1 Z规格说明语言支撑工具 240
12.1.1 Z/EVES 240
12.1.2 CADiZ 242
12.1.3 ZTC工具 243
12.1.4 Z User Studio 244
12.1.5 Zeus-Z工具 245
12.1.6 Z tools for Word 245
12.1.7 Z规格说明的动画工具 245
12.1.8 CZT项目 246
12.1.9其他Z支撑工具 246
12.2其他形式方法工具 247
12.2.1 PVS 247
12.2.2 Isabelle 247
12.2.3 SPIN 248
12.2.4 SMV 249
12.2.5 Alloy模型分析器 249
12.3其他形式方法及规格说明语言 250
12.3.1 B方法 250
12.3.2 Event-B方法 251
12.3.3维也纳开发方法 252
12.3.4 TCOZ语言 253
12.3.5 LOTOS语言 254
12.3.6 Larch语言 254
12.3.7通信顺序进程 255
12.3.8时段演算 256
12.3.9 UTP理论 256
12.3.10 SOFL方法 258
12.3.11 TLA+ 259
12.3.12 Petri网 259
小结 260
习题 260
附录A Z语法 262
附录B Z语言术语 265
附录C Object-Z语法 270
C. 1表示法 270
C. 2缩写 270
C. 3产生式 271
附录D部分习题解答 275
参考文献 296