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

目 次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