第1章 程序和精化
1．1 传统观点
1．2 一种新观点
1．3 程序作为契约：精化
1．4 抽象程序
1．5 可执行程序
1．6 混合程序
1．7 不可行程序
1．8 一些常见习惯用法
1．9 几个极端程序
1．10 练习
第2章 谓词演算
2．1 相关性
2．2 项
2．3 简单公式
2．4 命题公式
2．5 量词
2．6 (一般)公式
2．7 运算符的优先级
2．8 谓词演算
.2．9 练习
第3章 赋值和顺序复合
3．1 引言
3．2 赋值
3．3 开赋值
3．4 skip命令
3．5 顺序复合
3．6 赋值与复合的结合
3．7 例：交换变量的值
3．8 练习
第4章 选择
4．1 操作性描述
4．2 精化法则
4．3 练习
第5章 迭代
5．1 操作性描述
5．2 精化法则：非形式的
5．3 迭代的终止性：变动量
5．4 迭代的精化法则
5．5 迭代的"核查表"
5．6 练习
第6章 类型和声明
6．1 类型
6．2 声明
6．3 局部块
6．4 类型与不变式的使用
6．5 关于可行性的最后注记
6．6 类型和不变式的检查
6．7 无定义表达式
6．8 练习
第7章 实例研究：平方根
7．1 抽象程序：出发点
7．2 除去"外来"运算符
7．3 寻找不变式
7．4 练习
第8章 初始变量
8．1 简单规范
8．2 初始变量的精确化
8．3 再看顺序复合
8．4 先导赋值
8．5 练习
第9章 构造类型
9．1 幂集
9．2 包
9. 3 序列
9．4 分配运算符
9．5 函数
9．6 关系
9．7 练习
第10章 实例研究：插入排序
10．1 什么叫排序
10．2 类似的前后条件
10．3 减小变动量
10．4 向上或向下迭代
10．5 一个巧妙的不变式
10．6 对序列赋值
10．7 删除局部不变式
10．8 练习
第11章 过程和参数
11．1 无参过程
11．2 用值做替换
11．3 带参数的过程
11．4 对过程调用的精化
11．5 多重替换
11．6 值结果替换
11．7 语法问题
11．8 引用替换
11．9 练习
第12章 实例研究：堆排序
12．1 代码的时间复杂性
12．2 堆
12．3 堆的收缩
12．4 建堆
12．5 过程sift
12．6 练习
第13章 递归过程
13．1 部分正确性
13．2 递归的变动员
13．3 一个完整例子
13．4 跋：递归块
13．5 练月
第14章 实例研究：灰色编码
14．1 灰色编码
14．2 输入输出
14. 3 孤立的基础情况
14．4 练习
第13章 递归类型
15．1 不相交并
15．2 标志测试
15．3 对选择的模式匹配
15．4 类型声明
15．5 递归类型
15．6 结构序
15．7 迭代中的模式匹配
15．8 例子：树的求和
15．9 练习
第16章 模块和封装
16．1 模块声明
16．2 引出的和局部的过程
16．3 模块的精化
16．4 引入过程和变量
16．5 定义模块与实现模块
16．6 循环引出／引入
16．7 代码中的初始式
16．8 练习
第17章 状态变换和数据精化
17．1 我们还不能证明什么
17．2 状态变换
17．3 强制
17．4 加入变量：扩张
17．5 删除辅助变量：收缩
17．6 数据精化的一个实例
17．7 函数式抽象
17．8 练习
第18章 实例研究：多数表决
18．1 代码精化
18. 2 赢得选举
18．3 直接开发得到平方型代码
18．4 第二个尝试更快速
18．5 代码变换
18．6 简化的代码
18．7 练习
第19章 起源和总结
第20章 实 例研究：分段问题
20．1 均匀分段
20．2 最小损耗
20．3 生成均匀分段
20．4 练习
第21章 实例研究：直方图的最大矩形
21．1 做好基础性工作
21．2 分治法
21．3 强化不变式以恢复可行性
21．4 引入递归
21．5 包装
21．6 练习
第22章 实例研究：一个mail系统
22．1 第一个规范
22．2 标识符的重用
22．3 第二个规范：重用
22．4 第三个规范：延迟
22．5 第一个开发：异步发送
22．6 第二步开发：收条
22．7 最后的开发步骤：打包
22．8 练习
第23章 语义
23．1 引言
23．2 谓词变换器
23．3 语义定义
附录a 谓词演算的一些法则
a．1 一些命题法则
a．2 一些谓词法则
附录b 习题解答
附录c 法则汇编
参考文献
索引
· · · · · · (收起)