软件形式规格说明语言-Z2025|PDF|Epub|mobi|kindle电子书版本百度云盘下载

软件形式规格说明语言-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形式规格说明语言Z9

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为何需要面向对象的Z215

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/EVES240

12.1.2 CADiZ242

12.1.3 ZTC工具243

12.1.4 Z User Studio244

12.1.5 Zeus-Z工具245

12.1.6 Z tools for Word245

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

12.1.8 CZT项目246

12.1.9其他Z支撑工具246

12.2其他形式方法工具247

12.2.1 PVS247

12.2.2 Isabelle247

12.2.3 SPIN248

12.2.4 SMV249

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