从规范出发的程序设计（第2版）

　　本书详细论述了有关规范程序设计的内容，包括：程序和精化、谓词演算、选择、迭代、构造类型、模块和封装等，最后几章还包含了大量的实例研究和一些更高级的程序设计技术。本书提倡一种严格的程序开发方法，分析问题要用严格方式写出程序的规范，而后通过一系列具有严格理论基础的推导，最终得到可以运行的程序。 本书是被世界上许多重要大学采用的教材，适于计算机及相关专业的本科生和研究生使用。

　　裘宗燕知名译者，翻译严谨，喜与读者交流。裘宗燕教授是北京大学数学学院信息科学系的，关心的主要学术领域包括计算机软件理论、程序设计方法学、程序设计语言和符号计算。已出版多部著作和译著，包括《程序设计语言基础》（译著，1990），《Mathematica数学软件系统的应用与程序设计》（1994），《从问题到程序——程序设计与C语言引论》（1999）>>更多作品

第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  法则汇编                  
 参考文献                  
 索引