《程序设计方法学教程》求取 ⇩

绪论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