第1章 程序和精化 1
1.1 传统观点 1
1.2 一种新观点 1
1.3 程序作为契约：精化 2
1.4 抽象程序 3
1.5 可执行程序 7
1.6 混合程序 9
1.7 不可行程序 9
1.8 一些常见习惯用法 10
1.9 几个极端程序 11
1.10 练习 12
第2章 谓词演算 15
2.1 相关性 15
2.2 项 16
2.3 简单公式 16
2.4 命题公式 17
2.5 量词 18
2.6 （一般）公式 20
2.7 运算符的优先级 21
2.8 谓词演算 22
2.9 练习 24
3.2 赋值 26
第3章 赋值和顺序复合 26
3.1 引言 26
3.3 开赋值 28
3.4 skip 命令 28
3.5 顺序复合 29
3.6 赋值与复合的结合 30
3 7 例：交换变量的值 31
3.8 练习 32
第4章 选择 34
4.1 操作性描述 34
4.2 精化法则 35
4.3 练习 37
第5章 迭代 39
5.1 操作性描述 39
5.2 精化法则：非形式的 40
5.3 迭代的终止性：变动量 41
5.4 迭代的精化法则 43
5.5 迭代的“核查表” 44
5.6 练习 45
第6章 类型和声明 48
6.1 类型 48
6.2 声明 50
6.3 局部块 52
6.4 类型与不变式的使用 54
6.5 关于可行性的最后注记 55
6.6 类型和不变式的检查 56
6.7 无定义表达式 57
6.8 练习 57
第7章 实例研究：平方根 60
7.1 抽象程序：出发点 60
7.2 除去“外来”运算符 60
7.3 寻找不变式 61
7.4 练习 63
第8章 初始变量 64
8.1 简单规范 64
8.2 初始变量的精确化 65
8.3 再看顺序复合 66
8.4 先导赋值 67
8.5 练习 68
第9章 构造类型 70
9.1 幂集 70
9.2 包 73
9.3 序列 74
9.4 分配运算符 78
9.5 函数 80
9.6 关系 83
9.7 练习 86
第10章 实例研究：插入排序 90
10.1 什么叫排序 90
10.2 类似的前后条件 90
10.3 减小变动量 91
10.4 向上或向下迭代 92
10.5 一个巧妙的不变式 93
10.6 对序列赋值 95
10.8 练习 96
10.7 删除局部不变式 96
第11章 过程和参数 98
11.1 无参过程 99
11.2 用值做替换 101
11.3 带参数的过程 102
11.4 对过程调用的精化 103
11.5 多重替换 107
11.6 值结果替换 107
11.7 语法问题 109
11.8 引用替换 109
11.9 练习 110
第12章 实例研究：堆排序 112
12.1 代码的时间复杂性 112
12.2 堆 113
12.3 堆的收缩 114
12.4 建堆 115
12.5 过程Sift 116
12.6 练习 117
第13章 递归过程 119
13.1 部分正确性 119
13.2 递归的变动量 121
13.3 一个完整例子 122
13.4 跋：递归块 123
13.5 练习 125
第14章 实例研究：灰色编码 127
14.1 灰色编码 127
14.2 输入输出 128
14.3 孤立的基础情况 129
14.4 练习 130
第15章 递归类型 131
15.1 不相交并 131
15.2 标志测式 132
15.3 对选择的模式匹配 133
15.4 类型声明 136
15.5 递归类型 137
15.6 结构序 138
15.7 迭代中的模式匹配 139
15.8 例子：树的求和 141
15.9 练习 145
第16章 模块和封装 148
16.1 模块声明 148
16.2 引出的和局部的过程 149
16.3 模块的精化 150
16.4 引入过程和变量 151
16.5 定义模块与实现模块 153
15.6 循环引出／引入 154
16.7 代码中的初始式 154
16.8 练习 155
第17章 状态变换和数据精化 156
17.1 我们还不能证明什么 156
17.2 状态变换 157
17.3 强制 157
17.4 加入变量扩张 158
17.5 删除辅助变量：收缩 160
17.6 数据精化的一个实例 163
17.7 函数式抽象 166
17.8 练习 171
第18章 实例研究：多数表决 176
18.1 代码精化 176
18.2 赢得选举 177
18.3 直接开发得到平方型代码 177
18.4 第二个尝试更快速 180
18.5 代码变换 181
18.6 简化的代码 186
18.7 练习 188
第19章 起源和总结 189
第20章 实例研究：分段问题 192
20.1 均匀分段 192
20.2 最小损耗 194
20.3 生成均匀分段 197
20.4 练习 199
第21章 实例研究：直方图的最大矩形 201
21.1 做好基础性工作 201
21.2 分治法 202
21.3 强化不变式以恢复可行性 204
21.4 引入递归 205
21.6 练习 207
21.5 包装 207
第22章 实例研究：一个mail系统 209
22.1 第一个规范 210
22.2 标识符的重用 212
22.3 第二个规范：重用 215
22.4 第三个规范：延迟 216
22.5 第一个开发：异步发送 225
22.6 第二步开发：收条 229
22.7 最后的开发步骤：打包 231
22.8 练习 234
23.2 谓词变换器 238
第23章 语义 238
23.1 引言 238
23.3 语义定义 239
附录A 谓词演算的一些法则 247
A.1 一些命题法则 247
A.2 一些谓词法则 251
附录B 习题解答 255
附录C 法则汇编 285
参考文献 298
索引 300