形式化方法：理论及应用

目 录

前言

第一章 基础知识
1.1 集合. . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 关系与映射. . . . . . . . . . . . . . . . . . . . . 5
1.3 上下文无关文法. . . . . . . . . . . . . . . . . . 8
1.4 归纳法. . . . . . . . . . . . . . . . . . . . . . . . 12
1.5 归纳定义. . . . . . . . . . . . . . . . . . . . . . . 20
1.6 实现. . . . . . . . . . . . . . . . . . . . . . . . . 26
1.7 本章小结. . . . . . . . . . . . . . . . . . . . . . . 37
1.8 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 37
1.9 思考题. . . . . . . . . . . . . . . . . . . . . . . . 37

第二章 命题逻辑
2.1 语法. . . . . . . . . . . . . . . . . . . . . . . . . 41
2.2 证明系统. . . . . . . . . . . . . . . . . . . . . . . 44
2.3 构造逻辑. . . . . . . . . . . . . . . . . . . . . . . 51
2.4 语义系统. . . . . . . . . . . . . . . . . . . . . . . 55
2.5 可靠性和完备性定理. . . . . . . . . . . . . . . . 60
2.6 可判定性. . . . . . . . . . . . . . . . . . . . . . . 65
2.7 命题逻辑的实现. . . . . . . . . . . . . . . . . . 67
2.8 本章小结. . . . . . . . . . . . . . . . . . . . . . . 81
2.9 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 81
2.10 思考题. . . . . . . . . . . . . . . . . . . . . . . . 81

第三章 布尔可满足性
3.1 布尔可满足性. . . . . . . . . . . . . . . . . . . . 85
3.2 合取范式. . . . . . . . . . . . . . . . . . . . . . . 87
3.3 决议与传播. . . . . . . . . . . . . . . . . . . . . 93
3.4 DPLL 算法. . . . . . . . . . . . . . . . . . . . . . 96
3.5 实现. . . . . . . . . . . . . . . . . . . . . . . . . 98
3.6 本章小结. . . . . . . . . . . . . . . . . . . . . . . 108
3.7 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 108
3.8 思考题. . . . . . . . . . . . . . . . . . . . . . . . 109

第四章 谓词逻辑
4.1 命题的内部结构. . . . . . . . . . . . . . . . . . 111
4.2 语法. . . . . . . . . . . . . . . . . . . . . . . . . 112
4.3 证明系统. . . . . . . . . . . . . . . . . . . . . . . 121
4.4 语义系统. . . . . . . . . . . . . . . . . . . . . . . 126
4.5 可靠性和完备性. . . . . . . . . . . . . . . . . . 133
4.6 可判定性. . . . . . . . . . . . . . . . . . . . . . . 136
4.7 实现. . . . . . . . . . . . . . . . . . . . . . . . . 140
4.8 本章小结. . . . . . . . . . . . . . . . . . . . . . . 148
4.9 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 148
4.10 思考题. . . . . . . . . . . . . . . . . . . . . . . . 149

第五章 等式与未解释函数理论
5.1 可满足性模理论. . . . . . . . . . . . . . . . . . 153
5.2 等式与未解释函数理论. . . . . . . . . . . . . . 156
5.3 基本性质. . . . . . . . . . . . . . . . . . . . . . . 158
5.4 判定算法. . . . . . . . . . . . . . . . . . . . . . . 159
5.5 实现. . . . . . . . . . . . . . . . . . . . . . . . . 162
5.6 应用. . . . . . . . . . . . . . . . . . . . . . . . . 165
5.7 本章小结. . . . . . . . . . . . . . . . . . . . . . . 169
5.8 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 169
5.9 思考题. . . . . . . . . . . . . . . . . . . . . . . . 170

第六章 线性算术理论
6.1 语法. . . . . . . . . . . . . . . . . . . . . . . . . 175
6.2 高斯消元. . . . . . . . . . . . . . . . . . . . . . . 178
6.3 傅立叶-莫茨金消元. . . . . . . . . . . . . . . . . 180
6.4 单纯形法. . . . . . . . . . . . . . . . . . . . . . . 187
6.5 分支定界法. . . . . . . . . . . . . . . . . . . . . 194
6.6 减法逻辑. . . . . . . . . . . . . . . . . . . . . . . 196
6.7 实现. . . . . . . . . . . . . . . . . . . . . . . . . 197
6.8 应用. . . . . . . . . . . . . . . . . . . . . . . . . 204
6.9 本章小结. . . . . . . . . . . . . . . . . . . . . . . 211
6.10 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 211
6.11 思考题. . . . . . . . . . . . . . . . . . . . . . . . 212

第七章 数据结构理论
7.1 位向量. . . . . . . . . . . . . . . . . . . . . . . . 217
7.2 数组. . . . . . . . . . . . . . . . . . . . . . . . . 244
7.3 指针. . . . . . . . . . . . . . . . . . . . . . . . . 254
7.4 字符串. . . . . . . . . . . . . . . . . . . . . . . . 265
7.5 本章小结. . . . . . . . . . . . . . . . . . . . . . . 283
7.6 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 283
7.7 思考题. . . . . . . . . . . . . . . . . . . . . . . . 284

第八章 理论组合
8.1 理论组合. . . . . . . . . . . . . . . . . . . . . . . 289
8.2 Nelson-Oppen 协作过程. . . . . . . . . . . . . . 291
8.3 凸理论. . . . . . . . . . . . . . . . . . . . . . . . 296
8.4 非凸理论. . . . . . . . . . . . . . . . . . . . . . . 299
8.5 DPLL(T) 算法. . . . . . . . . . . . . . . . . . . . 302
8.6 实现. . . . . . . . . . . . . . . . . . . . . . . . . 305
8.7 本章小结. . . . . . . . . . . . . . . . . . . . . . . 309
8.8 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 309
8.9 思考题. . . . . . . . . . . . . . . . . . . . . . . . 309

第九章 符号执行
9.1 命令式语言IMP . . . . . . . . . . . . . . . . . . 313
9.2 操作语义. . . . . . . . . . . . . . . . . . . . . . . 316
9.3 符号执行. . . . . . . . . . . . . . . . . . . . . . . 327
9.4 混合执行. . . . . . . . . . . . . . . . . . . . . . . 334
9.5 符号执行工程. . . . . . . . . . . . . . . . . . . . 343
9.6 实现. . . . . . . . . . . . . . . . . . . . . . . . . 354
9.7 应用. . . . . . . . . . . . . . . . . . . . . . . . . 360
9.8 本章小结. . . . . . . . . . . . . . . . . . . . . . . 364
9.9 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 365
9.10 思考题. . . . . . . . . . . . . . . . . . . . . . . . 366

第十章 程序验证
10.1 霍尔三元组. . . . . . . . . . . . . . . . . . . . . 371
10.2 公理语义. . . . . . . . . . . . . . . . . . . . . . . 376
10.3 最弱前条件. . . . . . . . . . . . . . . . . . . . . 381
10.4 验证条件. . . . . . . . . . . . . . . . . . . . . . . 389
10.5 前向验证条件生成. . . . . . . . . . . . . . . . . 394
10.6 实现. . . . . . . . . . . . . . . . . . . . . . . . . 404
10.7 本章小结. . . . . . . . . . . . . . . . . . . . . . . 416
10.8 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 417
10.9 思考题. . . . . . . . . . . . . . . . . . . . . . . . 418

第十一章 程序合成
11.1 基本概念. . . . . . . . . . . . . . . . . . . . . . . 423
11.2 基于语法的合成. . . . . . . . . . . . . . . . . . 435
11.3 基于符号执行的合成. . . . . . . . . . . . . . . . 440
11.4 实现. . . . . . . . . . . . . . . . . . . . . . . . . 444
11.5 本章小结. . . . . . . . . . . . . . . . . . . . . . . 460
11.6 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 460
11.7 思考题. . . . . . . . . . . . . . . . . . . . . . . . 461

第十二章 Curry-Howard 同构
12.1 无类型λ 演算. . . . . . . . . . . . . . . . . . . . 465
12.2 简单类型化λ 演算. . . . . . . . . . . . . . . . . 472
12.3 Curry-Howard 同构. . . . . . . . . . . . . . . . . 483
12.4 二阶逻辑与系统F . . . . . . . . . . . . . . . . . 489
12.5 实现. . . . . . . . . . . . . . . . . . . . . . . . . 497
12.6 本章小结. . . . . . . . . . . . . . . . . . . . . . . 500
12.7 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 500
12.8 思考题. . . . . . . . . . . . . . . . . . . . . . . . 501

第十三章 依赖类型
13.1 基本概念. . . . . . . . . . . . . . . . . . . . . . . 503
13.2 纯一阶依赖类型. . . . . . . . . . . . . . . . . . 506
13.3 依赖总和类型. . . . . . . . . . . . . . . . . . . . 517
13.4 构造演算. . . . . . . . . . . . . . . . . . . . . . . 522
13.5 逻辑框架. . . . . . . . . . . . . . . . . . . . . . . 525
13.6 实现. . . . . . . . . . . . . . . . . . . . . . . . . 536
13.7 本章小结. . . . . . . . . . . . . . . . . . . . . . . 547
13.8 深入阅读. . . . . . . . . . . . . . . . . . . . . . . 547
13.9 思考题. . . . . . . . . . . . . . . . . . . . . . . . 548

参考文献