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

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