第1章绪论 1
1.1 软件与软件加工模型 1
目 录 1
1.1.1瀑布型 2
1.1.2快速原型 3
1.1.3 自动程序设计型 4
1.2形式方法 5
1.2.1 形式化和抽象的需要 5
1.2.2 形式方法与形式规格说明语言 6
1.2.3 形式方法的分类 6
1.2.4 形式方法的优缺点 7
1.3.1 Z语言是形式规格说明语言 8
1.2.5 软件开发过程中的形式方法 8
1.3 形式规格说明语言Z 8
1.3.2 Z规格说明简例 9
1.4小结 10
习题 10
第2章 一阶逻辑与集合论 11
2.1 命题逻辑 11
2.1.1 命题与联结词 11
2.1.2 命题公式与真值表 13
2.2谓词逻辑 14
2.2.1量词 14
2.2.2谓词公式 14
2.2.4 谓词公式的解释 15
2.2.3约束变量与自由变量 15
2.3 一阶逻辑中的证明 16
2.3.1 什么是证明？ 16
2.3.2 命题逻辑中的证明 17
2.3.3 命题逻辑中的定律 18
2.3.4 谓词逻辑中的证明 21
2.3.5 谓词逻辑中的定律 22
2.4集合论 25
2.4.1 集合的表示法 25
2.4.2集合谓词 26
2.4.3 空集、全集与幂集 26
2.4.4集合运算 27
习题 29
2.4.5 序偶与笛卡尔积 29
2.5小结 29
第3章 Z的类型与构造单元 31
3.1 Z的类型系统 31
3.1.1基本类型 32
3.1.2幂集类型 32
3.1.3 笛卡尔积类型 34
3.1.4 关于对象声明 35
3.1.5枚举类型 36
3.2 扩充表示法 37
3.2.1 量词化扩充表示法 37
3.2.2 集合表达式扩充表示法 38
3.2.3 Z的基本库 39
3.3.1 Z的符号 40
3.3 Z规格说明的构造单元 40
3.3.2公理描述 41
3.3.3模式 42
3.3.4 通用式定义 43
3.4小结 45
习题 45
第4章关系和函数 48
4.1关系 48
4.1.1关系表示法 49
4.1.2 定义域和值域 50
4.2关系的运算 52
4.2.1关系复合 52
4.2.2 恒等和闭包 54
4.2.3关系的逆 56
4.2.4 关系限定和限定减 56
4.2.5关系映象 59
4.3函数 61
4.3.1 部分函数与全函数 62
4.3.2 入射函数与满射函数 63
4.3.3 函数迭加操作和通用式定义 66
4.3.4 例——文具用品管理的模型 68
4.3.5λ－表示法 70
4.4小结 71
习题 71
5.1 模式的描述功能 77
5.1.1 模式描述抽象状态 77
第5章 模式和规格说明 77
5.1.2 模式描述操作 78
5.2 模式的修饰和包含 80
5.2.1 模式的修饰 80
5.2.2模式包含 81
5.2.3△和Ξ表示 81
5.2.4 初始状态模式 85
5.3模式运算 86
5.3.1 命题联结词连接模式 86
5.3.2模式复合 89
5.3.3 一个关于模式复合的例子 91
5.3.4前置条件模式 94
5.4.2 在声明中使用模式类型 96
5.4.1模式类型 96
5.4 模式类型和通用模式 96
5.4.3 通用式模式定义 98
5.5 规格说明文档的结构 100
5.6小结 102
习题 102
第6章 序列和包 105
6.1序列 105
6.1.1 序列表示和定义 106
6.1.2 连接和逆置操作 108
6.1.3 序列应用一——一个后备存储 110
6.1.4 head、ta i l、front和la s t操作 112
6.1.5 抽取、过滤、压缩和划分操作 114
6.1.6 序列应用二——一个正文编辑的规格说明 116
6.2.1 表示、定义和操作函数 123
6.2包 123
6.2.2 一个排序的规格说明 126
6.2.3 一个自动售货机的规格说明 127
6.3小结 133
习题 134
第7章 规格说明的实例 136
7.1简介 136
7.2 存储分配管理 137
7.2.1 系统状态描述 137
7.2.2 请求分配自由存储块的操作 138
7.2.3 释放一个存储块的操作 140
7.2.4 请求分配相邻的存储块集合 143
7.3.2 给定类型和枚举类型 145
7.3.1问题简介 145
7.3 图书馆数据库管理实例 145
7.3.3 抽象规格说明 146
7.4 自由类型的应用——命题逻辑证明器的规格说明 157
7.4.1 说明一个序列证明 158
7.4.2规格说明 160
7.5小结 161
习题 161
第8章 Z规格说明的形式推理 165
8.1 问题的提出和有关的概念 165
8.1.1 一个关于“学生兴趣小组”的规格说明 165
8.1.2 规格说明中的定理表示形式 168
8.2 关于严密证明 169
8.1.3 模式作为谓词 169
8.2.1 关于集合的推理 170
8.2.2 归归纳法证明 172
8.3一个定律库 175
8.4 关于规格说明的推理 178
8.4.1 引入一个“球迷身份卡” 178
8.4.2 初始化定理及其证明 179
8.4.3 前置条件及其简化 180
8.4.4 规格说明的性质及其证明 184
8.4.5 关于求精定理的证明 188
8.5小结 188
习题 189
9.1.1 存储管理程序的规格说明中的初始化定理 190
第9章 Z规格说明的若干推理实例 190
9.1 两个初始化定理的证明 190
9.1.2 图书馆数据库DB的初始化定理 191
9.2 两个前置条件的简化 192
9.2.1 存储管理程序中一个前置条件的简化 192
9.2.2 正文编辑程序中的一个前置条件的简化 194
9.3 规格说明中一般定理的证明 195
9.3.1 正文编辑程序中的一个定理 195
9.3.2 图书馆数据库管理系统中的一个定理 196
9.4小结 197
习题 197
10.1 程序范畴与软件求精 198
10.1.1程序范畴 198
第10章 从规格说明到程序代码 198
10.1.2软件求精 199
10.1.3 岗哨命令语言 199
10.1.4求精导向 200
10.2 Z规格说明的求精原则 201
10.2.1两种求精 201
10.2.2 简单过程求精 201
10.2.3 数据求精与过程求精 202
10.3 Z规格说明的求精示例 204
10.3.1 规格说明的第一步求精：设计分析 204
10.3.1.1 状态声明的设计 204
10.2.5小结 204
10.2.4 初始状态模式的求精 204
10.3.1.2 状态不变式的设计 206
10.3.1.3 第一步求精后的状态模式 206
10.3.1.4关联模式Ret rieve 208
10.3.1.5 初始状态模式 208
10.3.1.6 操作模式求精方法 208
10.3.1.7 操作模式成功部分的第一步求精 209
10.3.1.8 前置条件的第一步求精 210
10.3.1.9 出错处理部分的第一步求精 211
10.3.2 规格说明的第二步求精：算法设计 211
10.4小结 214
习题 215
11.1 Z规格说明支撑工具 216
11.1.1 CADi Z 216
第11章进一步的讨论 216
11.1.2 ZTC 217
11.1.3 zedB too1 219
11.2 关于规格说明的推理 219
11.3 Z规格说明语言与面向对象方法 220
11.3.1 Object-Z 220
11.3.2 Z++ 222
11.3.3 Z.S和OOZS 223
11.4 其他规格说明语言及形式方法的实践 225
11.4.1 其他规格说明语言 225
11.4.1.1 VDM语言 225
11.4.1.3 LOTOS语言 226
11.4.1.4 Larch语言 226
11.4.1.2 OBJ语言 226
11.4.1.5 Trace迹语言 227
11.4.1.6 GLI DE语言 227
11.4.1.7 ADTS语言 227
11.4.2 采用形式方法的实践 227
11.4.2.1 Cl ean room软件工程小组 227
11.4.2.2 MAPS半自动化程序构造系统 228
11.4.2.3其他 228
11.5结语 228
习题 229
参考文献 230
附录一Z语法 231
附录二 部分习题解答 235
索引 257