《软件工程语言-Z》求取 ⇩

第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 形式规格说明语言Z8

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 rieve208

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 Z216

第11章进一步的讨论216

11.1.2 ZTC217

11.1.3 zedB too1219

11.2 关于规格说明的推理219

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

11.3.1 Object-Z220

11.3.2 Z++222

11.3.3 Z.S和OOZS223

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