《程序验证和规范的形成方法》求取 ⇩

第一章引言1

1.1 形式方法1

1.2 验证问题1

1.3 规范问题2

1.4 程序构造与程序验证4

1.5 本书的组织7

第二章计算模型9

2.1 形式模型的性质9

2.2 抽象9

2.3 程序语义与抽象机10

2.4 抽象机11

2.5定义程序语义的方法12

2.5.1 操作方法12

2.5.2 指称方法14

2.5.3 公理方法15

2.5.4 三种验证方法的小结15

第三章验证方法19

3.1 术语与记号19

3.2 程序正确性22

3.3 语法单元正确性24

3.4 程序与语法单元26

3.5 测试与验证间的关系28

3.6验证技术32

3.6.1 执行函数的操作定义32

3.6.2 执行函数的指称定义34

3.6.3 执行函数的公理定义35

3.6.4 代数模拟37

第四章部分正确性的证明方法39

4.1 演绎系统：公理方法的数学基础39

4.2 公理方法的局限性41

4.3 公理正确性证明43

4.4归纳断言法44

4.4.1 解释45

4.4.2 谓词变换子与验证条件48

4.4.3 归纳断言定理53

4.5公理方法56

4.5.1 语义性质作为定理56

4.5.2 类ALGOL机的演绎系统57

4.5.3 证明过程61

4.5.4 评注64

第五章完全正确性的证明方法68

5.1 执行终止68

5.2 完全正确性与不可满足性70

5.3完全正确性与归纳断言法74

5.3.1 良序集74

5.3.2 完全正确性的归纳断言定理76

5.4完全正确性与公理方法78

5.4.1 迭代结构与部分正确性78

5.4.2 迭代结构与完全正确性84

5.4.3 评注87

5.5构造方法87

5.5.1 程序构造与正确性证明交替进行88

5.5.2 最弱前置条件89

5.5.3 程序设计演算92

5.5.4 程序设计演算的例子95

5.6 评注99

第六章并行程序的正确性105

6.1 并行程序所提出的问题105

6.2公理方法与并行程序110

6.2.1 互不干扰原理与显式同步110

6.2.2 隐式同步119

6.2.3 并行程序的完全正确性124

6.3 构造方法与并行程序127

6.4 通信顺序进程140

6.5 评注142

第七章验证方法的应用145

7.1发表过的证明145

7.1.1 数学函数146

7.1.2 分类、搜索和复杂的数据结构147

7.1.3 大型程序148

7.1.4 并行程序149

7.1.5 一个例子150

7.1.6 评价151

7.2拓广153

7.2.1 程序设计语言语义的定义153

7.2.2 定义一般语言结构成分的研究154

7.3 结论155

第八章规范方法157

8.1 规范的使用157

8.2 规范方法160

8.3代数规范162

8.3.1 有界栈的代数规范163

8.3.2 关于栈规范的注解164

8.3.3 代数规范方法的评论167

8.3.4 规范与验证之间的联系176

8.4状态机规范182

8.4.1 有界栈的状态机规范184

8.4.2 关于栈规范的注解185

8.4.3 状态机规范方法的评论188

8.4.4 规范与验证之间的联系200

8.5抽象模型规范204

8.5.1 序列的代数规范205

8.5.2 关于序列的代数规范的注解207

8.5.3 序列作为栈的抽象模型规范207

8.5.4 关于序列作为栈的模型的注解208

8.5.5 数组的代数规范210

8.5.6 数组作为栈的抽象模型规范211

8.5.7 关于数组作为栈的模型的注解212

8.5.8 抽象模型规范方法的评论213

8.5.9 规范与验证之间的联系214

8.6 几种方法的比较与等价217

第九章现状与总结222

9.1 概述222

9.2 软件的形式开发222

9.3理论在形式软件开发中的作用224

9.3.1 逻辑理论224

9.3.2 逻辑理论的现状225

9.3.3 构造理论226

9.4语言在形式软件开发中的作用230

9.4.1 规范语言的需求231

9.4.2 规范语言的现状231

9.4.3 程序设计语言的需求232

9.4.4 程序设计语言的现状233

9.5 工具在形式软件开发中的作用233

9.6 结束语236

参考文献238

名词索引246