从规范出发的程序设计(第2版)

从规范出发的程序设计(第2版)
作 者: Carroll Morgan 裘宗燕 裘宗燕
出版社: 机械工业出版社
丛编项: 软件工程技术丛书 前沿论题系列
版权说明: 本书为公共版权或经版权方授权,请支持正版图书
标 签: 暂缺
ISBN 出版时间 包装 开本 页数 字数
未知 暂无 暂无 未知 0 暂无

作者简介

  裘宗燕知名译者,翻译严谨,喜与读者交流。裘宗燕教授是北京大学数学学院信息科学系的,关心的主要学术领域包括计算机软件理论、程序设计方法学、程序设计语言和符号计算。已出版多部著作和译著,包括《程序设计语言基础》(译著,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 法则汇编

参考文献

索引