软件工程语言—Z

第1章 绪论
1、1软件与软件加工模型
1、1、1瀑布型
1、1、2快速原型
1、1、3自动程序设计型
1、2形式方法
1、2、1形式化和抽象的需要
1、2、2形式方法与形式规格说明语言
1、2、3形式方法的分类
1、2、4形式方法的优缺点
1、2、5软件开发过程中的形式方法
1、3形式规格说明语言Z
1、3、1Z语言是形式规格说明语言
1、3、2Z规格说明简例
1、4小结
习题
第2章 一阶逻辑与集合论
2、1命题逻辑
2、1、1命题与联结词
2、1、2命题公式与真值表
2、2谓词逻辑
2、2、1量词
2、2、2谓词公式
2、2、3约束变量与自由变量
2、2、4谓词公式的解释
2、3一阶逻辑中的证明
2、3、1什么是证明？
2、3、2命题逻辑中的证明
2、3、3命题逻辑中的定律
2、3、4谓词逻辑中的证明
2、3、5谓词逻辑中的定律
2、4集合论
2、4、1集合的表示法
2、4、2集合谓词
2、4、3空集、全集与幂集
2、4、4集合运算
2、4、5序偶与笛卡尔积
2、5小结
习题
第3章 Z的类型与构造单元
3、1Z的类型系统
3、1、1基本类型
3、1、2幂集类型
3、1、3笛卡尔积类型
3、1、4关于对象声明
3、1、5枚举类型
3、2扩充表示法
3、2、1量词化扩充表示法
3、2、2集合表达式扩充表示法
3、2、3Z的基本库
3、3Z规格说明的构造单元
3、3、1Z的符号
3、3、2公理描述
3、3、3模式
3、3、4通用式定义
3、4小结
习题
第4章 关系和函数
4、1关系
4、1、1关系表示法
4、1、2定义域和值域
4、2关系的运算
4、2、1关系复合
4、2、2恒等和闭包
4、2、3关系的逆
4、2、4关系限定和限定减
4、2、5关系映象
4、3函数
4、3、1部分函数与全函数
4、3、2入射函数与满射函数
4、3、3函数迭加操作和通用式定义
4、3、4例——文具用品管理的模型
4、3、5〓—表示法
4、4小结
习题
第5章 模式和规格说明
5、1模式的描述功能
5、1、1模式描述抽象状态
5、1、2模式描述操作
5、2模式的修饰和包含
5、2、1模式的修饰
5、2、2模式包含
5、2、3△和〓表示
5、2、4初始状态模式
5、3模式运算
5、3、1命题联结词连接模式
5、3、2模式复合
5、3、3一个关于模式复合的例子
5、3、4前置条件模式
5、4模式类型和通用模式
5、4、1模式类型
5、4、2在声明中使用模式类型
5、4、3通用式模式定义
5、5规格说明文档的结构
5、6小结
习题
第6章 序列和包
6、1序列
6、1、1序列表示和定义
6、1、2连接和逆置操作
6、1、3序列应用一——一个后备存储
6、1、4head、tail、front和last操作
6、1、5抽取、过滤、压缩和划分操作
6、1、6序列应用二——一个正文编辑的规格说明
6、2包
6、2、1表示、定义和操作函数
6、2、2一个排序的规格说明
6、2、3一个自动售货机的规格说明
6、3小结
习题
第7章 规格说明的实例
7、1简介
7、2存储分配管理
7、2、1系统状态描述
7、2、2请求分配自由存储块的操作
7、2、3释放一个存储块的操作
7、2、4请求分配相邻的存储块集合
7、3图书馆数据库管理实例
7、3、1问题简介
7、3、2给定类型和枚举类型
7、3、3抽象规格说明
7、4自由类型的应用——命题逻辑证明器的规格说明
7、4、1说明一个序列证明
7、4、2规格说明
7、5小结
习题
第8章 Z规格说明的形式推理
8、1问题的提出和有关的概念
8、1、1一个关于“学生兴趣小组”的规格说明
8、1、2规格说明中的定理表示形式
8、1、3模式作为谓词
8、2关于严密证明
8、2、1关于集合的推理
8、2、2归纳法证明
8、3一个定律库
8、4关于规格说明的推理
8、4、1引入一个“球迷身份卡”
8、4、2初始化定理及其证明
8、4、3前置条件及其简化
8、4、4规格说明的性质及其证明
8、4、5关于求精定理的证明
8、5小结
习题
第9章 Z规格说明的若干推理实例
9、1两个初始化定理的证明
9、1、1存储管理程序的规格说明中的初始化定理
9、1、2图书馆数据库DB的初始化定理
9、2两个前置条件的简化
9、2、1存储管理程序中一个前置条件的简化
9、2、2正文编辑程序中的一个前置条件的简化
9、3规格说明中一般定理的证明
9、3、1正文编辑程序中的一个定理
9、3、2图书馆数据库管理系统中的一个定理
9、4小结
习题
第10章 从规格说明到程序代码
10、1程序范畴与软件求精
10、1、1程序范畴
10、1、2软件求精
10、1、3岗哨命令语言
10、1、4求精导向
10、2Z规格说明的求精原则
10、2、1两种求精
10、2、2简单过程求精
10、2、3数据求精与过程求精
10、2、4初始状态模式的求精
10、2、5小结
10、3Z规格说明的求精示例
10、3、1规格说明的第一步求精：设计分析
10、3、1、1状态声明的设计
10、3、1、2状态不变式的设计
10、3、1、3第一步求精后的状态模式
10、3、1、4关联模式Retrieve
10、3、1、5初始状态模式
10、3、1、6操作模式求精方法
10、3、1、7操作模式成功部分的第一步求精
10、3、1、8前置条件的第一步求精
10、3、1、9出错处理部分的第一步求精
10、3、2规格说明的第二步求精：算法设计
10、4小结
习题
第11章 进一步的讨论
11、1Z规格说明支撑工具
11、1、1CADiZ
11、1、2ZTC
11、1、3zedBtool
11、2关于规格说明的推理
11、3Z规格说明语言与面向对象方法
11、3、1Object—Z
11、3、2〓
11、3、3Z．S和OOZS
11、4其他规格说明语言及形式方法的实践
11、4、1其他规格说明语言
11、4、1、1VDM语言
11、4、1、2OBJ语言
11、4、1、3LOTOS语言
11、4、1、4Larch语言
11、4、1、5Trace迹语言
11、4、1、6GLIDE语言
11、4、1、7ADTS语言
11、4、2采用形式方法的实践
11、4、2、1Cleanroom软件工程小组
11、4、2、2MAPS半自动化程序构造系统
11、4、2、3其他
11、5结语
习题
参考文献
附录一Z语法
附录二部分习题解答
索引
var cpro_id = 'u317582';