从规范出发的程序设计PDF电子书下载

第1章 程序和精化 1

1.1 传统观点 1

1.2 一种新观点 1

1.3 程序作为契约：精化 2

1.4 抽象程序 3

1.5 可执行程序 7

1.6 混合程序 9

1.7 不可行程序 9

1.8 一些常见习惯用法 10

1.9 几个极端程序 11

1.10 练习 12

第2章 谓词演算 15

2.1 相关性 15

2.2 项 16

2.3 简单公式 16

2.4 命题公式 17

2.5 量词 18

2.6 （一般）公式 20

2.7 运算符的优先级 21

2.8 谓词演算 22

2.9 练习 24

3.2 赋值 26

第3章 赋值和顺序复合 26

3.1 引言 26

3.3 开赋值 28

3.4 skip 命令 28

3.5 顺序复合 29

3.6 赋值与复合的结合 30

3 7 例：交换变量的值 31

3.8 练习 32

第4章 选择 34

4.1 操作性描述 34

4.2 精化法则 35

4.3 练习 37

第5章 迭代 39

5.1 操作性描述 39

5.2 精化法则：非形式的 40

5.3 迭代的终止性：变动量 41

5.4 迭代的精化法则 43

5.5 迭代的“核查表” 44

5.6 练习 45

第6章 类型和声明 48

6.1 类型 48

6.2 声明 50

6.3 局部块 52

6.4 类型与不变式的使用 54

6.5 关于可行性的最后注记 55

6.6 类型和不变式的检查 56

6.7 无定义表达式 57

6.8 练习 57

第7章 实例研究：平方根 60

7.1 抽象程序：出发点 60

7.2 除去“外来”运算符 60

7.3 寻找不变式 61

7.4 练习 63

第8章 初始变量 64

8.1 简单规范 64

8.2 初始变量的精确化 65

8.3 再看顺序复合 66

8.4 先导赋值 67

8.5 练习 68

第9章 构造类型 70

9.1 幂集 70

9.2 包 73

9.3 序列 74

9.4 分配运算符 78

9.5 函数 80

9.6 关系 83

9.7 练习 86

第10章 实例研究：插入排序 90

10.1 什么叫排序 90

10.2 类似的前后条件 90

10.3 减小变动量 91

10.4 向上或向下迭代 92

10.5 一个巧妙的不变式 93

10.6 对序列赋值 95

10.8 练习 96

10.7 删除局部不变式 96

第11章 过程和参数 98

11.1 无参过程 99

11.2 用值做替换 101

11.3 带参数的过程 102

11.4 对过程调用的精化 103

11.5 多重替换 107

11.6 值结果替换 107

11.7 语法问题 109

11.8 引用替换 109

11.9 练习 110

第12章 实例研究：堆排序 112

12.1 代码的时间复杂性 112

12.2 堆 113

12.3 堆的收缩 114

12.4 建堆 115

12.5 过程Sift 116

12.6 练习 117

第13章 递归过程 119

13.1 部分正确性 119

13.2 递归的变动量 121

13.3 一个完整例子 122

13.4 跋：递归块 123

13.5 练习 125

第14章 实例研究：灰色编码 127

14.1 灰色编码 127

14.2 输入输出 128

14.3 孤立的基础情况 129

14.4 练习 130

第15章 递归类型 131

15.1 不相交并 131

15.2 标志测式 132

15.3 对选择的模式匹配 133

15.4 类型声明 136

15.5 递归类型 137

15.6 结构序 138

15.7 迭代中的模式匹配 139

15.8 例子：树的求和 141

15.9 练习 145

第16章 模块和封装 148

16.1 模块声明 148

16.2 引出的和局部的过程 149

16.3 模块的精化 150

16.4 引入过程和变量 151

16.5 定义模块与实现模块 153

15.6 循环引出／引入 154

16.7 代码中的初始式 154

16.8 练习 155

第17章 状态变换和数据精化 156

17.1 我们还不能证明什么 156

17.2 状态变换 157

17.3 强制 157

17.4 加入变量扩张 158

17.5 删除辅助变量：收缩 160

17.6 数据精化的一个实例 163

17.7 函数式抽象 166

17.8 练习 171

第18章 实例研究：多数表决 176

18.1 代码精化 176

18.2 赢得选举 177

18.3 直接开发得到平方型代码 177

18.4 第二个尝试更快速 180

18.5 代码变换 181

18.6 简化的代码 186

18.7 练习 188

第19章 起源和总结 189

第20章 实例研究：分段问题 192

20.1 均匀分段 192

20.2 最小损耗 194

20.3 生成均匀分段 197

20.4 练习 199

第21章 实例研究：直方图的最大矩形 201

21.1 做好基础性工作 201

21.2 分治法 202

21.3 强化不变式以恢复可行性 204

21.4 引入递归 205

21.6 练习 207

21.5 包装 207

第22章 实例研究：一个mail系统 209

22.1 第一个规范 210

22.2 标识符的重用 212

22.3 第二个规范：重用 215

22.4 第三个规范：延迟 216

22.5 第一个开发：异步发送 225

22.6 第二步开发：收条 229

22.7 最后的开发步骤：打包 231

22.8 练习 234

23.2 谓词变换器 238

第23章 语义 238

23.1 引言 238

23.3 语义定义 239

附录A 谓词演算的一些法则 247

A.1 一些命题法则 247

A.2 一些谓词法则 251

附录B 习题解答 255

附录C 法则汇编 285

参考文献 298

索引 300