软件形式规格说明语言-ZPDF电子书下载

第1章 绪论 1

1.1软件生命周期 2

1.2存在的问题 4

1.3形式方法 4

1.3.1形式化和抽象的需要 4

1.3.2什么是形式方法 5

1.3.3形式验证技术 5

1.3.4形式方法发展的历史简介 6

1.3.5形式规格说明语言的分类 6

1.3.6形式方法的应用 7

1.3.7推荐使用形式方法的相关标准 7

1.3.8形式方法的优缺点 8

1.4形式规格说明语言Z 9

1.4.1 Z语言概述 9

1.4.2 Z规格说明简例 9

小结 10

习题 11

第2章 一阶逻辑与集合论 12

2.1命题逻辑 12

2.1.1命题与连接词 12

2.1.2命题公式与真值表 14

2.2谓词逻辑 14

2.2.1量词 15

2.2.2谓词公式 15

2.2.3约束变量与自由变量 15

2.2.4谓词公式的解释 16

2.3一阶逻辑中的证明 16

2.3.1什么是证明 17

2.3.2命题逻辑中的证明 17

2.3.3命题逻辑中的定律 19

2.3.4谓词逻辑中的证明 22

2.3.5谓词逻辑中的定律 22

2.4集合论 26

2.4.1集合的表示法 26

2.4.2集合谓词 26

2.4.3空集、全集与幂集 27

2.4.4集合运算 27

2.4.5序偶与笛卡儿积 29

小结 30

习题 30

第3章Z的类型与构造单元 31

3.1 Z的类型系统 31

3.1.1基本类型 31

3.1.2幂集类型 32

3.1.3笛卡儿积类型 33

3.1.4对象声明 34

3.1.5枚举类型 35

3.2扩充表示法 36

3.2.1量词化扩充表示法 36

3.2.2集合表达式扩充表示法 37

3.2.3 Z的基本库 38

3.3 Z规格说明的构造单元 39

3.3.1 Z的符号 39

3.3.2公理定义 40

3.3.3模式 41

3.3.4通用式定义 42

小结 44

习题 44

第4章 关系和函数 48

4.1关系 48

4.1.1关系表示法 49

4.1.2定义域和值域 50

4.2关系的运算 51

4.2.1关系复合 52

4.2.2恒等和闭包 53

4.2.3关系的逆 55

4.2.4关系限定和限定减 56

4.2.5关系映像 58

4.3函数 59

4.3.1部分函数与全函数 60

4.3.2入射函数与满射函数 61

4.3.3函数叠加操作和通用式定义 64

4.3.4文具用品管理的模型示例 66

4.3.5 λ-表示法 68

小结 68

习题 69

第5章 模式和规格说明 74

5.l模式的描述功能 74

5.1.1模式描述抽象状态 74

5.1.2模式描述操作 75

5.2模式的修饰和包含 76

5.2.1模式的修饰 76

5.2.2模式包含 77

5.2.3Δ和？表示 78

5.2.4初始状态模式 80

5.3模式运算 81

5.3.1命题连接词连接模式 81

5.3.2模式复合 84

5.3.3一个关于模式复合的例子 86

5.3.4前置条件模式 89

5.4模式类型和通用模式 90

5.4.1模式类型 90

5.4.2在声明中使用模式类型 91

5.4.3通用式模式定义 92

5.5规格说明文档的结构 93

小结 95

习题 96

第6章 序列和包 98

6.1序列 98

6.1.1序列表示和定义 98

6.1.2连接和逆置操作 100

6.1.3序列应用一——一个后备存储 103

6.1.4 head、tail、front和last操作 104

6.1.5抽取、过滤、压缩和划分操作 106

6.1.6序列应用二——一个正文编辑的规格说明 108

6.2包 114

6.2.1包表示、定义和操作函数 114

6.2.2一个排序的规格说明 117

6.2.3一个自动售货机的规格说明 118

小结 124

习题 124

第7章 规格说明的实例 128

7.1简介 128

7.2存储分配管理 129

7.2.1系统状态描述 129

7.2.2请求分配空闲存储块的操作 130

7.2.3释放一个存储块的操作 132

7.2.4请求分配相邻的存储块集合 134

7.3图书馆数据库管理实例 136

7.3.1问题简介 136

7.3.2给定类型和枚举类型 136

7.3.3抽象规格说明 137

7.4自由类型的应用——命题逻辑证明器的规格说明 148

7.4.1说明一个序列证明 148

7.4.2规格说明 150

小结 151

习题 151

第8章 Z规格说明的形式推理 155

8.1问题的提出和有关的概念 155

8.1.1一个关于“学生兴趣小组”的规格说明 155

8.1.2规格说明中的定理表示形式 158

8.1.3模式作为谓词 158

8.2关于严密证明 159

8.2.1关于集合的推理 159

8.2.2归纳法证明 162

8.3一个定律库 164

8.4关于规格说明的推理 167

8.4.1引入一个“球迷身份卡” 168

8.4.2初始化定理及其证明 168

8.4.3前置条件及其简化 170

8.4.4规格说明的性质及其证明 173

8.4.5关于精化定理的证明 177

小结 177

习题 177

第9章Z规格说明的若干推理实例 179

9.1两个初始化定理的证明 179

9.1.1存储管理程序的规格说明中的初始化定理 179

9.1.2图书馆数据库DB的初始化定理 179

9.2两个前置条件的简化 181

9.2.1存储管理程序中一个前置条件的简化 181

9.2.2正文编辑程序中的一个前置条件的简化 182

9.3规格说明中一般定理的证明 183

9.3.1正文编辑程序中的一个定理 183

9.3.2图书馆数据库管理系统中的一个定理 185

小结 185

习题 186

第10章 从规格说明到程序 187

10.1程序范畴与软件精化 187

10.1.1程序范畴 187

10.1.2软件精化 188

10.1.3岗哨命令语言 188

10.1.4精化导向 189

10.2 Z规格说明的精化原则 190

10.2.1两种精化 190

10.2.2操作精化 190

10.2.3数据精化 192

10.2.4数据精化实例 194

10.2.5小结 197

10.3精化演算 198

10.3.1赋值语句 199

10.3.2条件语句 201

10.3.3逻辑常量 202

10.3.4顺序复合 202

10.3.5循环语句 203

10.4 Z的精化演算方法 204

10.5实例研究 207

10.5.1形式规格说明 207

10.5.2数据精化 208

10.5.3转换为精化演算的抽象程序 210

10.5.4操作精化 211

小结 212

习题 213

第11章Object-Z规格说明语言 215

11.1为何需要面向对象的Z 215

11.2 Object-Z语言简介 217

11.2.1语法定义 217

11.2.2被继承类 219

11.2.3局部定义 219

11.2.4状态模式 219

11.2.5初始状态模式 220

11.3操作 221

11.3.1操作模式 221

11.3.2操作提升 223

11.3.3操作运算符 223

11.3.4实例说明 225

11.4分布运算符 226

11.5递归定义 227

11.6继承 228

11.7对象包含 230

11.8多态性 231

11.9类合并 232

11.9.1定义类合并 233

11.9.2多态核心 233

11.9.3实例：电动工具 233

11.9.4类合并与多态运算符的区别 235

11.10 self常量 235

11.11 Obj ect-Z语言的工具支持 236

11.12 Object-Z实例研究：银行系统 237

小结 238

习题 238

第12章 形式方法及其工具 240

12.1 Z规格说明语言支撑工具 240

12.1.1 Z/EVES 240

12.1.2 CADiZ 242

12.1.3 ZTC工具 243

12.1.4 Z User Studio 244

12.1.5 Zeus-Z工具 245

12.1.6 Z tools for Word 245

12.1.7 Z规格说明的动画工具 245

12.1.8 CZT项目 246

12.1.9其他Z支撑工具 246

12.2其他形式方法工具 247

12.2.1 PVS 247

12.2.2 Isabelle 247

12.2.3 SPIN 248

12.2.4 SMV 249

12.2.5 Alloy模型分析器 249

12.3其他形式方法及规格说明语言 250

12.3.1 B方法 250

12.3.2 Event-B方法 251

12.3.3维也纳开发方法 252

12.3.4 TCOZ语言 253

12.3.5 LOTOS语言 254

12.3.6 Larch语言 254

12.3.7通信顺序进程 255

12.3.8时段演算 256

12.3.9 UTP理论 256

12.3.10 SOFL方法 258

12.3.11 TLA+ 259

12.3.12 Petri网 259

小结 260

习题 260

附录A Z语法 262

附录B Z语言术语 265

附录C Object-Z语法 270

C. 1表示法 270

C. 2缩写 270

C. 3产生式 271

附录D部分习题解答 275

参考文献 296