程序验证和规范的形成方法PDF电子书下载

第一章 引言 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