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