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

目 次 1

导论 1

0.1 本书的结构 1

0.2程序设计方法学发展回顾 3

第一部分程序逻辑基础 7

第一章程序规范与程序正确性 9

1.1断言与规范 9

1.2程序的执行状态 11

1.3数组的解释 13

1.4程序正确性证明梗概 14

练 习 17

第二章最弱前置谓词与程序语言￡的语义 18

2.1最弱前置谓词 18

2.2基本语句的定义 19

2.2.1 空语句 20

2.2.2赋值语句 20

2.2.3顺序复合 21

2.2.4 选择语句 21

2.2.5循环语句 22

*2.3多重赋值语句的定义 26

*2.4过程调用的定义 27

练 习 30

第三章程序设计基本方法 33

3.1面向目标的程序设计 34

3.2选择语句的设计 34

3.3循环程序的设计 35

3.4不变式构造 37

3.4.1 削弱ψ就ρ：删除合取分量 37

3.4.2削弱ψ就ρ：变量替换常量 37

3.4.3削弱ψ就ρ：扩大变量变化范围 38

3.4.4联合？与ψ就ρ 39

3.5界函数 39

*3.6略述大型程序之设计 40

练 习 42

第四章程序正确性验证：公理学方法 45

4.1程序正确性与部分正确性 45

4.2 Hoare系统 45

4.3“正向”证明和“反向”证明 47

*4.4协调性与完全性 49

*4.5关于“完全”正确性的证明系统 50

练习 51

*4.6 Hoare系统的扩充 51

第五章并行程序验证：时态逻辑方法 53

5.1 引言 53

5.2时态逻辑一般概念 54

5.2.1模态逻辑框架 55

5.2.2时态逻辑框架 56

5.2.3程序时态逻辑 57

5.2.4模型 58

5.3.1并行程序模型 60

5.2.5若干有效时态公式 60

5.3并行程序及其执行 60

5.3.2并行性及其交叉模拟 62

5.3.3信号灯 64

5.3.4公正性 65

5.4并行程序性质的时态描述 66

5.4.1不变性 68

5.4.2活动性 72

5.4.3优先性质 74

练 习 76

*第六章并行程序的时态证明系统 78

6.1时态逻辑系统 78

6.1.1时态命题逻辑 78

6.1.2时态谓词逻辑 82

6.1.3带等词的时态谓词逻辑 83

6.1.4框架公理和规则 84

6.2论域系统 85

6.3程序公理和推理规则 86

6.4.1分布计算最大公约数 88

6.4举例子 88

6.4.2信号灯 90

6.4.3互斥 91

6.5证明原理 92

6.5.1不变性原理 92

6.5.2活动性原理 93

6.5.3优先性质证明原理 96

练习 97

第一部分参考文献 97

第二部分模型规范与程序开发 99

7.1软件开发的形式化 101

第七章概论 101

7.2软件系统规范描述的一般原则 102

7.3模型抽象与多步开发过程 105

7.4偏函数逻辑 106

7.4.1 问题的背景 106

7.4.2偏函数逻辑的模型理论 106

7.4.3偏函数逻辑的证明理论 108

练 习 113

8.1.1 函数的规范 115

8.1运算的规范描述 115

第八章模型抽象与规范描述 115

8.1.2运算的规范 117

8.2结构归纳法与集合抽象 118

8.2.1结构归纳法 119

8.2.2集合表示及其推理 120

8.2.3规范描述举例 122

8.3模型规范：基于状态的数据类型 124

8.4结构类型、映射抽象及序列抽象 125

8.4.1结构类型与规范描述 125

8.4.2映射抽象与规范描述 129

8.4.3序列抽象与规范描述 132

8.5表示抽象的重要性：关于模型构造方法的一点讨论 134

练习 136

第九章模型具体化与程序开发 139

9.1数据类型的精化 139

9.1.1抽象函数与充分性 140

9.1.2数据精化的正确性 142

9.1.3数据精化的例 144

9.2模型的实现偏倾及讨论 146

9.3运算的分解 148

9.3.1分而治之与组装式开发方法 149

9.3.2关于运算分解的证明规则 149

9.3.3运算分解的例 150

练习 151

第二部分参考文献 151

第三部分大型程序设计 153

第十章大型程序设计与抽象数据类型 155

10.1大型程序设计概述 155

10.1.1大型程序的特点 155

10.1.3模块分解准则 156

10.1.2什么是大型程序设计 156

10.2数据抽象发展的背景与动机 157

10.3 Ada 中的数据抽象模块——程序包 161

10.3.1 程序包的基本特点 161

10.3.2程序包的三种模块形式 165

10.4类属程序包与抽象数据类型的参数化 170

10.5 Ada程序结构 173

练 习 176

11.1抽象数据类型的规范描述 178

第十一章抽象数据类型的形式规范描述 178

*11.2 Hoare公理方法 179

11.3代数公理方法 182

11.3.1 举例 183

11.3.2代数规范描述的形式定义 185

11.3.3 代数规范描述的设计 186

11.4代数规范描述的协调性与完全性 191

11.4.1协调性 191

11.4.2完全性 193

练习 194

12.1.1 ∑——代数 196

12.1代数与范畴 196

*第十二章代数规范描述的语义模型 196

12.1.2范畴与函子 199

12.2语义模型的选择 201

12.3初始代数语义 202

12.4终止代数语义 203

12.5关于语义模型的几点评注 204

12.6 正确性 205

12.7实现 207

12.7.1 直接实现 208

12.7.2非直接实现 211

12.8参数化规范描述及语义模型 213

练 习 216

第十三章大型程序的组装 218

13.1界面、实现、模块 219

*13.2 Pebble语言简介 224

13.2.1基本特征 225

13.2.2 相关类型 227

*13.3模块的组装 229

练 习 232

第三部分参考文献 232