目录

第一篇 绪论

（一）程序设计方法学及其重要性

（二）几种程序设计方法简介

第二篇 预备知识

第一章 程序状态及有关状态转换的定理

1.1 谓词演算中的有关知识

1.2 程序状态及断言

1.3 文字代换和状态转换定理

1.4 介绍一种程序说明形式

习题一

第二章 程序正确性的证明及其证明法则

2.1 关于程序正确性的证明

2.2 程序证明提纲

2.3 程序正确性证明法则

2.4 小规模程序设计

习题二

3.1 一维数组的函数观点

第三章 数组的标记方法及有关约定

3.2 数组段和图形表示法

§3.3 多维数组处理法

习题三

第三篇 一个小型语言的语义

第四章 谓词转换和skip语句、abort语句

4.1 谓词转换算子wp

4.2 skip语句、abort语句和复合语句

习题四

5.1 简单变量的赋值

第五章 赋值语句

5.2 简单变量的多重赋值

5.3 数组元素的赋值

5.4 一般的多重赋值语句

习题五

第六章 选择语句和迭代语句

6.1 选择语句

6.2 关于选择语句的定理及其应用

6.3 常规的while循环和迭代语句

6.4 DO的形式定义

6.5 关于循环、不变式和限界函数的定理

6.6 如何注解循环和如何理解这些注解

习题六

第七章 过程调用

7.1 具有值参数和结果参数的调用

7.2 关于过程调用的定理

7.3 使用变量参数

7.4 允许后置条件中出现值参数

习题七

8.1 从目标断言推导程序

第八章 程序的推导技术

第四篇 程序研制

8.2 从不变式和限界函数推导循环

习题八

第九章 求循环不变式的方法

9.1 气球理论

9.2 删去一个合取项

9.3 用变量代替后置条件中的常量

9.4 用扩大变量值域的方法求循环不变式

9.5 把前置条件和后置条件组合起来求循环不变式

9.6 限界函数的进一步讨论

习题九

第十章 递归算法转化为迭代算法

10.1 化繁为简

10.2 分而治之

10.3 实例——遍历二叉树

习题十

第十一章 程序质量问题初议

11.1 限制不确定性

11.2 从循环体中抽出断言

11.3 改变数据表示方法提高程序效率

11.4 文档编制的一般规则

习题十

第十二章 两个较大的实例

12.1 字符串文件编辑过程中的向右对齐问题

12.2 最长递增序列

习题十二

第十三章 程序的逆

习题十三

参考文献