第一部分 数学 1
第1章 数学推理 1
1.1 形式推理 1
1.1.1 相继式和谓词 1
1.1.2 推理规则 2
1.1.3 证明 3
1.1.4 基本规则 3
1.2 命题演算 5
1.2.1 基本断言的记法形式 5
1.2.2 命题逻辑的推理规则 6
1.2.3 一些证明 8
1.2.4 一个证明过程 14
1.2.5 扩充记法形式 16
1.2.6 一些经典结果 18
1.3 谓词演算 18
1.3.1 量化谓词和代换的记法形式 18
1.3.2 全称量化公式 20
1.3.3 非自由性 20
1.3.4 代换 21
1.3.5 谓词演算的推理规则 23
1.3.6 若干证明 23
1.3.7 扩充的证明过程 24
1.3.8 存在量化公式 25
1.3.9 一些经典结果 26
1.4 等式 27
1.5 有序对 30
1.6 练习 33
第2章 集合形式 35
2.1 基本集合结构 36
2.1.1 语法 36
2.1.2 公理 38
2.1.3 性质 39
2.2 类型检查 41
2.3 派生结构 46
2.3.1 定义 46
2.3.2 实例 46
2.3.3 类型检查 47
2.3.4 性质 48
2.4 二元关系 49
2.4.1 二元关系结构：第一组 49
2.4.2 二元关系结构：第二组 51
2.4.3 二元关系结构的实例 52
2.4.4 二元关系结构的类型检查 53
2.5 函数 54
2.5.1 函数构造：第一组 55
2.5.2 函数构造：第二组 57
2.5.3 函数构造的示例 57
2.5.4 函数求值的性质 58
2.5.5 函数构造的类型检查 60
2.6 分类的性质 60
2.6.1 有关成员关系的法则 61
2.6.2 单调性法则 62
2.6.3 包含法则 63
2.6.4 相等法则 64
2.7 例子 77
2.8 练习 81
参考文献 82
第3章 数学对象 83
3.1 广义的交和并 83
3.2 构造数学对象 88
3.2.1 非形式的引言 88
3.2.2 不动点 88
3.2.3 归纳原理 92
3.3 一个集合的有穷子集的集合 96
3.4 有穷集合和无穷集合 98
3.5.1 定义 99
3.5 自然数 99
3.5.2 皮阿诺“公理” 101
3.5.3 最小值 105
3.5.4 强归纳原理 108
3.5.5 最大值 109
3.5.6 自然数上的递归函数 109
3.5.7 算术 111
3.5.8 关系的迭代 115
3.5.9 有穷集的势 115
3.5.10 关系的传递闭包 116
3.6 整数 117
3.7 有穷序列 119
3.7.1 归纳构造 119
3.7.2 直接构造 121
3.7.3 序列上的运算 121
3.7.4 排序及相关问题 125
3.7.5 整数序列的字典序 129
3.8 有穷树 129
3.8.1 非形式的介绍 129
3.8.2 形式化构造 130
3.8.3 归纳 132
3.8.4 递归 134
3.8.5 运算 136
3.8.6 树的表达 137
3.9 标记树 140
3.9.1 直接定义 140
3.9.2 归纳定义 140
3.9.3 归纳 142
3.9.4 递归 142
3.9.5 递归定义的运算 143
3.10 二叉树 144
3.10.1 直接的运算 144
3.9.6 直接定义的运算 144
3.10.2 归纳 145
3.10.3 递归 145
3.10.4 递归定义的运算 145
3.11 良构关系 146
3.11.1 定义 147
3.11.2 在良构集上通过归纳进行证明 147
3.11.3 在良构集上的递归 148
3.11.4 良构性的证明 151
3.11.5 一个良构关系实例 152
3.11.6 非经典递归的其他实例 152
3.12 练习 153
第二部分 抽象机 156
第4章 抽象机引论 156
4.1 抽象机 157
4.2 静态行为——描述状态 157
4.3 动态行为——描述操作 158
4.4 将前－后谓词作为规范 159
4.5 证明义务 159
4.6 代换作为规范 160
4.7 前条件代换（终止性） 161
4.8 参数化和初始化 162
4.9 带有输入参数的操作 164
4.10 带有输出参数的操作 165
4.11 规范的宽松风格和防御风格 165
4.12 多重简单代换 167
4.13 条件代换 168
4.14 约束选择代换 168
4.15 卫式代换（可行性） 169
4.16 没有任何作用的代换 170
4.17 上下文信息——集合和常量 170
4.18 无约束选择代换 173
4.19 显式定义 176
4.20 断言 179
4.21 具体变量和抽象常量 180
4.22 练习 181
参考文献 182
第5章 抽象机的定义 183
5.1 广义代换 183
5.1.1 语法 183
5.1.2 类型检查 186
5.1.3 公理 187
5.2 抽象机 188
5.2.1 语法 188
5.2.3 类型检查 189
5.2.2 可见性规则 189
5.2.4 关于常量 191
5.2.5 证明义务 192
5.2.6 关于给定集合和预定义常量 193
参考文献 194
第6章 抽象机理论 195
6.1 规范型 195
6.2 两个有用的性质 198
6.3 终止性、可行性和前－后谓词 199
6.3.1 终止性 199
6.3.2 可行性 201
6.3.3 前－后谓词 202
6.4 集合论模型 204
6.4.1 第一个模型——一个集合和一个关系 204
6.4.2 第二个模型——集合变换器 206
6.4.3 各种结构的集合论解释 209
6.5 练习 210
第7章 大型抽象机 212
7.1 多重广义代换 212
7.1.1 定义 212
7.1.2 基本性质 213
7.1.3 主要结果 215
7.2 规范的递增描述 216
7.2.1 非形式的介绍 216
7.2.2 操作调用 217
7.2.3 INCLUDES子句 219
7.2.4 可见性规则 220
7.2.5 传递性 220
7.2.6 机器的重命名 221
7.2.7 PROMOTES和EXTENDS子句 221
7.2.8 实例 221
7.3 递增的规范描述和规范共享 222
7.3.1 非形式的介绍 222
7.3.3 可见性规则 223
7.3.2 USES子句 223
7.3.4 传递性 224
7.3.5 机器重命名 224
7.4 形式定义 224
7.4.1 语法 224
7.4.2 类型检查 225
7.4.3 INCLUDES子句的证明义务 229
7.4.4 USES子句的证明义务 231
7.5 练习 233
8.1.1 非形式的规范 234
8.1 一个货单系统 234
第8章 抽象机的实例 234
8.1.2 机器Client 235
8.1.3 机器Product 236
8.1.4 机器Invoice 238
8.1.5 机器Invoice_System 241
8.2 电话交换机 242
8.2.1 非形式的规范 242
8.2.2 机器Simple_Exchange 244
8.2.3 机器Exchange 247
8.3 电梯控制系统 249
8.3.1 非形式的规范 249
8.3.2 机器Lift 250
8.3.3 活性（liveness）的证明 254
8.3.4 活性证明义务的表述 255
8.4 练习 257
参考文献 257
第三部分 程序设计 258
第9章 顺序和循环 258
9.1 顺序 258
9.1.1 语法 258
9.1.2 公理 258
9.1.3 基本性质 259
9.2.1 引论 261
9.2 循环 261
9.2.2 定义 262
9.2.3 循环终止的解释 264
9.2.4 循环的前－后关系的解释 267
9.2.5 循环终止的实例 268
9.2.6 不变式定理 268
9.2.7 变动量定理 269
9.2.8 变动量和不变式定理的进一步实用化 271
9.2.9 传统循环 272
9.3 练习 277
10.0.1 重用前面的算法 280
第10章 程序设计实例 280
10.0 方法学 280
10.0.2 循环结构的证明规则 282
10.0.3 顺序结构的证明规则 283
10.1 无约束搜索 283
10.1.1 引言 283
10.1.2 比较两个序列 286
10.1.3 计算一个函数的自然数逆 290
10.1.4 自然数的除法 292
10.1.5 递归函数的特殊情况 294
10.1.6 给定底的对数 296
10.1.7 整数平方根 297
10.2 有约束搜索 298
10.2.1 引言 298
10.2.2 线性搜索 300
10.2.3 在数组中的线性搜索 302
10.2.4 在矩阵里的线性检索 303
10.2.5 二分搜索 304
10.2.6 再论单调函数 307
10.2.7 数组里的二分搜索 311
10.3 自然数 314
10.3.1 基本模式 314
10.3.3 扩展基本模式 315
10.3.2 自然数求幂 315
10.3.4 对序列求和 317
10.3.5 子数列移位 318
10.3.6 向排序的数组中插入 320
10.4 序列 321
10.4.1 引言 321
10.4.2 累计序列里的元素 323
10.4.3 数的基数表示 325
10.4.4 将自然数转换为基数表示 326
10.4.5 二元运算的快速计算 329
10.4.6 左递归和右递归 332
10.4.7 过滤器 335
10.5 树 343
10.5.1 公式的记法 343
10.5.2 将树变换到公式 344
10.5.3 从树变换到波兰表示串 346
10.5.4 将公式变换到波兰表示串 347
10.6 练习 353
参考文献 355
11.1.1 非形式的讨论 356
11.1 广义代换的精化 356
第11章 精化 356
第四部分 精化 356
11.1.2 形式定义 357
11.1.3 广义代换的相等 358
11.1.4 单调性 358
11.1.5 广义赋值的精化 359
11.2 抽象机的精化 361
11.2.1 非形式的讨论 361
11.2.2 形式定义 364
11.2.3 充分条件 364
11.2.4 单调性 368
11.2.5 实例重温 372
11.2.6 最后的润色 373
11.2.7 精化条件的直观解释 378
11.2.8 对小例子的应用 379
11.3 形式定义 380
11.3.1 语法 380
11.3.2 类型检查 381
11.3.3 证明义务 384
11.4 练习 386
参考文献 392
12.1.1 引言 394
12.1 精化的实现 394
第12章 构造大型抽象机 394
12.1.2 有关引入的实际考虑 397
12.1.3 IMPLEMENTATION结构 399
12.1.4 IMPORTS 子句 400
12.1.5 可见性规则 401
12.1.6 机器重命名 401
12.1.7 VALUES 子句 401
12.1.8 IMPORTS和INCLUDES子句的比较 403
12.1.9 PROMOTES和EXTENDS子句 403
12.1.10 再论具体常量和具体变量 403
12.1.11 在实现中允许出现的各种结构 404
12.2 共享 409
12.2.1 引言 409
12.2.2 SEES子句 412
12.2.3 可见性 412
12.2.4 传递性和循环定义 413
12.2.5 机器重命名 413
12.2.6 USES 子句和SEES子句的比较 414
12.3 再论循环结构 414
12.4 多重精化和实现 414
12.5 递归定义的操作 416
12.5.1 引言 417
12.5.3 证明规则 419
12.5.2 语法 419
12.6 形式证明 421
12.6.1 一个IMPLEMENTATION的语法 421
12.6.2 对 IMPORTS 子句的类型检查 422
12.6.3 对SEES子句的类型检查 423
12.6.4 一个IMPLEMENTATION的证明义务 423
12.6.5 对SEES子句的证明义务 426
13.1 一个基本机器库 427
13.1.1 机器BASIC_CONSTANTS 427
第13章 精化的实例 427
13.1.2 机器BASIC_IO 428
13.1.3 机器BASIC_BOOL 428
13.1.4 机器BASIC_enum 429
13.1.5 机器BASIC_FILE_VAR 429
13.2 实例研究：数据库系统 430
13.2.1 有关文件的机器 432
13.2.2 有关对象的机器 440
13.2.3 一个数据库 445
13.2.4 界面 450
13.3.2 机器SEQUENCE_VAR 457
13.3.1 机器ARRAY_VAR 457
13.3 一个实用的抽象机库 457
13.3.3 机器SET_VAR 458
13.3.4 机器ARRAY_ECTION 458
13.3.5 机器SEQUENCE_COLLECTION 458
13.3.6 机器SET ECTION 459
13.3.7 机器TREE_VAR 459
13.4 实例研究：锅炉控制系统 463
13.4.1 引言 463
13.4.2 非形式的规范 464
13.4.3 系统分析 467
13.4.4 系统集成 473
13.4.5 形式化规范和设计 475
13.4.6 最后的体系结构 485
13.4.7 修改初始规范 486
参考文献 488
附录 489
附录A 记法综述 489
附录B 语法 493
附录C 定义 500
附录D 可见性规则 510
附录E 规则和公理 514
附录F 证明义务 520