第一章 可计算性 1
引言 1
1-1 有限自动机 2
1-1.1 正则表达式 4
1-1.2 有限自动机 8
1-1.3 转换图 10
1-1.4 克林定理 12
1-1.5 等价定理 18
1-2 图林机 22
1-2.1 图林机 23
1-2.2 波斯特机 26
1-2.3 带有下推存贮器的有限机 32
1-2.4 不确定性 38
1-3 图林机作为接受器 41
1-3.1 递归可枚举集 42
1-3.2 递归集 43
1-3.3 形式语言 45
1-4 图林机作为生成器 49
1-4.1 原始递归函数 50
1-4.2 部分递归函数 57
1-5 图林机作为算法 60
1-5.1 是／否问题类的可解性 62
1-5.2 图林机的停机问题 63
1-5.3 半图厄系统的字问题 66
1-5.4 波斯特对应问题 69
1-5.5 是／否问题类的部分可解性 74
文献述评 77
参考文献 78
习题 80
第二章 谓词演算 89
引言 89
2-1 基本概念 93
2-1.1 语法 93
2-1.2 语义（解释） 99
2-1.3 有效的wff 105
2-1.4 wff的等价 112
2-1.5 wff的范式 120
2-1.6 有效性问题 124
2-2 自然演绎法 128
2-2.1 联结词规则 130
2-2.2 量词规则 137
2-2.3 运算符规则 146
2-3 分解法 150
2-3.1 子句形式 151
2-3.2 赫尔布兰德过程 156
2-3.3 一致算法 164
2-3.4 分解规则 169
文献述评 174
参考文献 175
习题 177
第三章 程序的验证 196
引言 196
3-1 框图程序 196
3-1.1 部分正确性 206
3-1.2 终止 219
3-2 带数组的框图程序 227
3-2.1 部分正确性 227
3-2.2 终止 234
3-3 类ALGOL程序 243
3-3.1 当型程序 243
3-3.2 部分正确性 246
3-3.3 全正确性 253
文献述评 261
参考文献 262
习题 265
引言 284
第四章 框图模式 284
4-1 基本概念 285
4-1.1 语法 285
4-1.2 语义（解释） 287
4-1.3 基本性质 292
4-1.4 赫尔布兰德解释 303
4-2 判定问题 306
4-2.1 基本性质的不可解性 308
4-2.2 自由模式 313
4-2.3 树模式 319
4-2.4 亚诺夫（Ianov）模式 328
4-3 用谓词演算作形式化 338
4-3.1 算法 338
4-3.2 框图程序性质的形式化 350
4-3.3 框图模式性质的形式化 355
4-4 转换问题 362
4-4.1 递归模式 364
4-4.2 框图模式与递归模式 368
文献述评 379
参考文献 380
习题 382
第五章 程序的不动点理论 401
引言 401
5-1 函数和泛函 402
5-1.1 单调函数 404
5-1.2 连续泛函 412
5-1.3 泛函的不动点 416
5-2 递归程序 421
5-2.1 计算规则 422
5-2.2 不动点计算规则 431
5-2.3 递归定义组 438
5-3 验证方法 441
5-3.1 逐步计算归纳法 441
5-3.2 完全计算归纳法 449
5-3.3 不动点归纳法 453
5-3.4 结构归纳法 459
文献述评 468
参考文献 469
习题 471
附第一篇论文：程序的逻辑分析 484
附第二篇论文：计算机程序设计的逻辑方法 534
参考文献 615