目录 1
第一篇 绪论 1
（一）程序设计方法学及其重要性 1
（二）几种程序设计方法简介 4
第二篇 预备知识 15
第一章 程序状态及有关状态转换的定理 15
1.1 谓词演算中的有关知识 15
1.2 程序状态及断言 18
1.3 文字代换和状态转换定理 23
1.4 介绍一种程序说明形式 26
习题一 28
第二章 程序正确性的证明及其证明法则 30
2.1 关于程序正确性的证明 30
2.2 程序证明提纲 31
2.3 程序正确性证明法则 34
2.4 小规模程序设计 37
习题二 38
3.1 一维数组的函数观点 39
第三章 数组的标记方法及有关约定 39
3.2 数组段和图形表示法 42
§3.3 多维数组处理法 44
习题三 47
第三篇 一个小型语言的语义 49
第四章 谓词转换和skip语句、abort语句 49
4.1 谓词转换算子wp 49
4.2 skip语句、abort语句和复合语句 53
习题四 54
5.1 简单变量的赋值 56
第五章 赋值语句 56
5.2 简单变量的多重赋值 58
5.3 数组元素的赋值 60
5.4 一般的多重赋值语句 62
习题五 65
第六章 选择语句和迭代语句 69
6.1 选择语句 69
6.2 关于选择语句的定理及其应用 72
6.3 常规的while循环和迭代语句 74
6.4 DO的形式定义 75
6.5 关于循环、不变式和限界函数的定理 80
6.6 如何注解循环和如何理解这些注解 81
习题六 83
第七章 过程调用 87
7.1 具有值参数和结果参数的调用 87
7.2 关于过程调用的定理 90
7.3 使用变量参数 96
7.4 允许后置条件中出现值参数 98
习题七 99
8.1 从目标断言推导程序 105
第八章 程序的推导技术 105
第四篇 程序研制 105
8.2 从不变式和限界函数推导循环 112
习题八 125
第九章 求循环不变式的方法 128
9.1 气球理论 128
9.2 删去一个合取项 130
9.3 用变量代替后置条件中的常量 133
9.4 用扩大变量值域的方法求循环不变式 141
9.5 把前置条件和后置条件组合起来求循环不变式 145
9.6 限界函数的进一步讨论 149
习题九 153
第十章 递归算法转化为迭代算法 157
10.1 化繁为简 158
10.2 分而治之 161
10.3 实例——遍历二叉树 165
习题十 172
第十一章 程序质量问题初议 174
11.1 限制不确定性 174
11.2 从循环体中抽出断言 177
11.3 改变数据表示方法提高程序效率 182
11.4 文档编制的一般规则 190
习题十 210
第十二章 两个较大的实例 211
12.1 字符串文件编辑过程中的向右对齐问题 211
12.2 最长递增序列 219
习题十二 224
第十三章 程序的逆 228
习题十三 240
参考文献 241