软件工程语言-ZPDF电子书下载

第1章绪论 1

1.1 软件与软件加工模型 1

目 录 1

1.1.1瀑布型 2

1.1.2快速原型 3

1.1.3 自动程序设计型 4

1.2形式方法 5

1.2.1 形式化和抽象的需要 5

1.2.2 形式方法与形式规格说明语言 6

1.2.3 形式方法的分类 6

1.2.4 形式方法的优缺点 7

1.3.1 Z语言是形式规格说明语言 8

1.2.5 软件开发过程中的形式方法 8

1.3 形式规格说明语言Z 8

1.3.2 Z规格说明简例 9

1.4小结 10

习题 10

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

2.1 命题逻辑 11

2.1.1 命题与联结词 11

2.1.2 命题公式与真值表 13

2.2谓词逻辑 14

2.2.1量词 14

2.2.2谓词公式 14

2.2.4 谓词公式的解释 15

2.2.3约束变量与自由变量 15

2.3 一阶逻辑中的证明 16

2.3.1 什么是证明？ 16

2.3.2 命题逻辑中的证明 17

2.3.3 命题逻辑中的定律 18

2.3.4 谓词逻辑中的证明 21

2.3.5 谓词逻辑中的定律 22

2.4集合论 25

2.4.1 集合的表示法 25

2.4.2集合谓词 26

2.4.3 空集、全集与幂集 26

2.4.4集合运算 27

习题 29

2.4.5 序偶与笛卡尔积 29

2.5小结 29

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

3.1 Z的类型系统 31

3.1.1基本类型 32

3.1.2幂集类型 32

3.1.3 笛卡尔积类型 34

3.1.4 关于对象声明 35

3.1.5枚举类型 36

3.2 扩充表示法 37

3.2.1 量词化扩充表示法 37

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

3.2.3 Z的基本库 39

3.3.1 Z的符号 40

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

3.3.2公理描述 41

3.3.3模式 42

3.3.4 通用式定义 43

3.4小结 45

习题 45

第4章关系和函数 48

4.1关系 48

4.1.1关系表示法 49

4.1.2 定义域和值域 50

4.2关系的运算 52

4.2.1关系复合 52

4.2.2 恒等和闭包 54

4.2.3关系的逆 56

4.2.4 关系限定和限定减 56

4.2.5关系映象 59

4.3函数 61

4.3.1 部分函数与全函数 62

4.3.2 入射函数与满射函数 63

4.3.3 函数迭加操作和通用式定义 66

4.3.4 例——文具用品管理的模型 68

4.3.5λ－表示法 70

4.4小结 71

习题 71

5.1 模式的描述功能 77

5.1.1 模式描述抽象状态 77

第5章 模式和规格说明 77

5.1.2 模式描述操作 78

5.2 模式的修饰和包含 80

5.2.1 模式的修饰 80

5.2.2模式包含 81

5.2.3△和Ξ表示 81

5.2.4 初始状态模式 85

5.3模式运算 86

5.3.1 命题联结词连接模式 86

5.3.2模式复合 89

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

5.3.4前置条件模式 94

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

5.4.1模式类型 96

5.4 模式类型和通用模式 96

5.4.3 通用式模式定义 98

5.5 规格说明文档的结构 100

5.6小结 102

习题 102

第6章 序列和包 105

6.1序列 105

6.1.1 序列表示和定义 106

6.1.2 连接和逆置操作 108

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

6.1.4 head、ta i l、front和la s t操作 112

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

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

6.2.1 表示、定义和操作函数 123

6.2包 123

6.2.2 一个排序的规格说明 126

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

6.3小结 133

习题 134

第7章 规格说明的实例 136

7.1简介 136

7.2 存储分配管理 137

7.2.1 系统状态描述 137

7.2.2 请求分配自由存储块的操作 138

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

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

7.3.2 给定类型和枚举类型 145

7.3.1问题简介 145

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

7.3.3 抽象规格说明 146

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

7.4.1 说明一个序列证明 158

7.4.2规格说明 160

7.5小结 161

习题 161

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

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

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

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

8.2 关于严密证明 169

8.1.3 模式作为谓词 169

8.2.1 关于集合的推理 170

8.2.2 归归纳法证明 172

8.3一个定律库 175

8.4 关于规格说明的推理 178

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

8.4.2 初始化定理及其证明 179

8.4.3 前置条件及其简化 180

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

8.4.5 关于求精定理的证明 188

8.5小结 188

习题 189

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

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

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

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

9.2 两个前置条件的简化 192

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

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

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

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

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

9.4小结 197

习题 197

10.1 程序范畴与软件求精 198

10.1.1程序范畴 198

第10章 从规格说明到程序代码 198

10.1.2软件求精 199

10.1.3 岗哨命令语言 199

10.1.4求精导向 200

10.2 Z规格说明的求精原则 201

10.2.1两种求精 201

10.2.2 简单过程求精 201

10.2.3 数据求精与过程求精 202

10.3 Z规格说明的求精示例 204

10.3.1 规格说明的第一步求精：设计分析 204

10.3.1.1 状态声明的设计 204

10.2.5小结 204

10.2.4 初始状态模式的求精 204

10.3.1.2 状态不变式的设计 206

10.3.1.3 第一步求精后的状态模式 206

10.3.1.4关联模式Ret rieve 208

10.3.1.5 初始状态模式 208

10.3.1.6 操作模式求精方法 208

10.3.1.7 操作模式成功部分的第一步求精 209

10.3.1.8 前置条件的第一步求精 210

10.3.1.9 出错处理部分的第一步求精 211

10.3.2 规格说明的第二步求精：算法设计 211

10.4小结 214

习题 215

11.1 Z规格说明支撑工具 216

11.1.1 CADi Z 216

第11章进一步的讨论 216

11.1.2 ZTC 217

11.1.3 zedB too1 219

11.2 关于规格说明的推理 219

11.3 Z规格说明语言与面向对象方法 220

11.3.1 Object-Z 220

11.3.2 Z++ 222

11.3.3 Z.S和OOZS 223

11.4 其他规格说明语言及形式方法的实践 225

11.4.1 其他规格说明语言 225

11.4.1.1 VDM语言 225

11.4.1.3 LOTOS语言 226

11.4.1.4 Larch语言 226

11.4.1.2 OBJ语言 226

11.4.1.5 Trace迹语言 227

11.4.1.6 GLI DE语言 227

11.4.1.7 ADTS语言 227

11.4.2 采用形式方法的实践 227

11.4.2.1 Cl ean room软件工程小组 227

11.4.2.2 MAPS半自动化程序构造系统 228

11.4.2.3其他 228

11.5结语 228

习题 229

参考文献 230

附录一Z语法 231

附录二 部分习题解答 235

索引 257