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

点此进入-本书在线PDF格式电子书下载【推荐-云解压-方便快捷】直接下载PDF格式图书。移动端-PC端通用
种子下载[BT下载速度快] 温馨提示：（请使用BT下载软件FDM进行下载）软件下载地址页 直链下载[便捷但速度慢]   [在线试读本书]   [在线获取解压码]

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

下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。

建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如 BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！

（文件页数 要大于 标注页数，上中下等多册电子书除外）

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

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