软件形式规格说明语言—Z

第1章　绪论
1．1软件生命周期
1．2存在的问题
1．3形式方法
1．4形式规格说明语言z
小结
习题第2章　一阶逻辑与集合论
2．1命题逻辑
2．2谓词逻辑
2．3一阶逻辑中的证明
2．4集合论
小结
习题第3章　z的类型与构造单元
3．1z的类型系统
3．2扩充表示法
3．3z规格说明的构造单元
小结
习题第4章　关系和函数
4．1关系
4．2关系的运算
4．3函数
小结
习题第5章　模式和规格说明
5．1模式的描述功能
5．2模式的修饰和包含
5．3模式运算
5．4模式类型和通用模式
5．5规格说明文档的结构
小结
习题第6章　序列和包
6．1序列
6．2包
小结
习题第7章　规格说明的实例
7．1简介
7．2存储分配管理
7．3图书馆数据库管理实例
7．4自由类型的应用——命题逻辑证明器的规格说明
小结
习题第8章　z规格说明的形式推理
8．1问题的提出和有关的概念
8．2关于严密证明
8．3一个定律库
8．4关于规格说明的推理
小结
习题第9章　z规格说明的若干推理实例
9．1两个初始化定理的证明
9．2两个前置条件的简化
9．3规格说明中一般定理的证明
小结
习题第10章　从规格说明到程序
10．1程序范畴与软件精化
10．2z规格说明的精化原则
10．3精化演算
10．4z的精化演算方法
10．5实例研究
小结
习题第11章　object-z规格说明语言
11．1为何需要面向对象的z
11．2object—z语言简介
11．3操作
11．4分布运算符
11．5递归定义
11．6继承
11．7对象包含
11．8多态性
11．9类合并
11．10self常量
11．11object—z语言的工具支持
11．12object—z实例研究：银行系统
小结
习题第12章　形式方法及其工具
12．1z规格说明语言支撑工具
12．2其他形式方法工具
12．3其他形式方法及规格说明语言
小结
习题附录az语法
附录bz语言术语
附录cobject-z语法
c．1表示法
c．2缩写
c．3产生式
附录d部分习题解答
参考文献