程序设计方法学教程PDF电子书下载

绪论 1

一、程序设计的短暂历史回顾 1

二、结构程序设计 1

三、证明程序正确 2

四、构造正确程序 3

第一章 结构程序 4

第一节 流图程序 4

一、程序的有向图表示 4

二、真程序 5

第二节 程序函数 5

一、执行图和执行树 5

二、程序函数 6

四、单调函数的复合 6

二、复合程序 10

一、素程序 10

第三节 结构定理 10

三、结构定理 11

四、递归结构程序 12

第四节 层次化控制结构 14

一、while型程序结构 14

二、PDL结构 14

三、程序非正常退出和循环非正常退出 15

四、程序的结构化变换 16

第五节 读结构程序 18

一、程序阅读方法 18

二、读素程序 19

三、逐步抽象阅读 21

四、结构程序的逻辑注释 24

习题 25

三、程序正确性 30

二、规范问题 30

第二章 程序验证——归纳断言法 30

第一节 基本慨念 30

一、程序验证 30

四、中间断言 31

第二节 反向代换技术 31

一、路径函数 31

二、反向代换 31

三、路径部分正确性 32

第三节 部分正确性证明的归纳断言法 33

一、部分正确性的归纳断言定理 33

二、部分正确性证明算法 34

三、数组对程序验证的影响 36

第四节 终结性证明 41

一、良基集合 41

二、良断言与良函数 41

三、良基集合法 42

习题 44

第一节 Hoare的公理化方法 46

一、归纳表达式 46

二、验证规则 46

第三章 和序验证——公理化方法 46

三、验址规则定理 47

第二节 终结规则法 49

一、终结规则 49

二、终结规则定理 50

第三节 谓词转换器 53

一、一种非确定性程序设计语言 53

二、最弱前置条件 54

三、程序证明的演绎系统 55

四、终结性和正确性验证 56

习题 58

二、单调函数 60

一、定义域和值域的扩充 60

第一节 函数 60

第四章 程序验证——不动点方法 60

三、自然扩充 61

五、最小上界 62

第二节 泛函 63

一、单调性与连续性 63

二、泛函的不动点 64

第三节 递归程序 65

一、计算法则 65

二、不动点计算法则 67

第四节 递归程守的验证方法 67

一、逐步计算归纳 67

二、完全计算归纳 69

三、不动点归纳 71

四、结构归纳 73

习题 75

第五章 构造正确程序 79

第一节 利用不变式构造程序 79

第二节 不变式的推导技术 84

第三节 程序设计演算 87

习题 91

第六章 形式规范技术 93

第一节 规范语言 93

一、规范与程序 93

二、规范语言的要求 93

三、规范语言的一个实例 94

四、存在性和唯一性 96

五、哲学家问题的规范 96

第二节 抽象数据类型 98

一、类型抽象 98

二、抽象类型规范方法分类 98

三、Hoare方法 99

四、代数方法 101

五、代数规范的一致性和完备性 104

习题 105

第七章 逐步求精开发程序 106

第一节 逐步求精方法 106

第二节 非递归程序的开发 106

第三节 递归程序的开发 116

第四节 逐步求精方法总结 120

习题 121

第八章 程序变换 122

第一节 基本概念 122

一、程序等价 122

二、程序段、程序图式扣图代变量 122

四、程序变换的基本原理 123

五、程序变换语言 123

三、程序变换规则既述 123

第二节 基本变换规则 124

一、扩展(unfold)相折叠(fold) 124

二、定义(definition)规则 124

五、抽象(abstraction)规则 125

六、改写规则 125

第三节 由谓词定义式向函数定义式的变换 125

四、定律(law) 125

三、取样(instantiation)规则 125

第四节 函数定义级上的变换 128

一、减少递归函数的应用性表现的变换 128

二、把一些递归变换成尾递归 129

第五节 函数定义级向过程级变换 130

第六节 过程级变换 131

第七节 程序变换系统 131

习题 132

参考文献 133