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

　　形式方法是一种基于数学的软件开发方法。形式规格说明是形式方法最基本的部分，它精确描述用户需求和计算机软件系统的功能，并用于软件验证和精化。z是目前颇受欢迎且使用较广泛的一种形式规格说明语言。本书旨在讨论软件工程中形式方法的概念、方法和表示法，并详细介绍z的类型系统、数学语言和公理定义、通用式定义、模式等结构，还讨论了z规格说明的推理和求精方法。本书还介绍了面向对象的规格说明语言object—z和其他形式方法表示和工具。全书结构合理、内容丰富、实例详尽多样。各章配有习题。《软件形式规格说明语言—z》可作为计算机、软件工程、信息安全和信息管理等专业本科生和研究生的教材，也可作为大专院校有关专业的教师参考书，还可作为从事软件工程、软件开发和软件应用的研究人员和技术人员的参考资料。

暂缺《软件形式规格说明语言—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部分习题解答
参考文献