第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 法则汇编
参考文献
索引
鄂公网安备 42010302001612号 