软件形式规格说明语言-Z/软件工程专业核心课程系列教材

《普通高等教育"十一五"国家级规划教材？软件工程专业核心课程系列教材:软件形式规格说明语言(Z)》可作为计算机、软件工程、信息安全和信息管理等专业本科生和研究生的教材，也可作为大专院校有关专业的教师参考书，还可作为从事软件工程、软件开发和软件应用的研究人员和技术人员的参考资料。

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

第1章绪论
1.1软件生命周期
1.2存在的问题
1.3形式方法
1.3.1形式化和抽象的需要
1.3.2什么是形式方法
1.3.3形式验证技术
1.3.4形式方法发展的历史简介
1.3.5形式规格说明语言的分类
1.3.6形式方法的应用
1.3.7推荐使用形式方法的相关标准
1.3.8形式方法的优缺点
1.4形式规格说明语言2
1.4.1Z语言概述
1.4.22规格说明简例
小结
习题
第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序偶与笛卡儿积
小结
习题
第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.32规格说明的构造单元
3.3.1Z的符号
3.3.2公理定义
3.3.3模式
3.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λ—表示法
小结
习题
第5章模式和规格说明
5.1模式的描述功能
5.1.1模式描述抽象状态
5.1.2模式描述操作
5.2模式的修饰和包含
5.2.1模式的修饰
5.2.2模式包含
5.2.3A和巳表示
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规格说明文档的结构
小结
习题
第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一个自动售货机的规格说明
小结
习题
第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规格说明
小结
习题
第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关于精化定理的证明
小结
习题
第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图书馆数据库管理系统中的一个定理
小结
习题
第10章从规格说明到程序
10.1程序范畴与软件精化
10.1.1程序范畴
10.1.2软件精化
10.1.3岗哨命令语言
10.1.4精化导向
10.22规格说明的精化原则
10.2.1两种精化
10.2.2操作精化
10.2.3数据精化
10.2.4数据精化实例
10.2.5小结
10.3精化演算
10.3.1赋值语句
10.3.2条件语句
10.3.3逻辑常量
10.3.4顺序复合
10.3.5循环语句
10.4Z的精化演算方法
10.5实例研究
10.5.1形式规格说明
10.5.2数据精化
10.5.3转换为精化演算的抽象程序
10.5.4操作精化
小结
习题
第11章Object—Z规格说明语言
11.1为何需要面向对象的Z
11.2Object—Z语言简介
11.2.1语法定义
11.2.2被继承类
11.2.3局部定义
11.2.4状态模式
11.2.5初始状态模式
11.3操作
11.3.1操作模式
11.3.2操作提升
11.3.3操作运算符
11.3.4实例说明
11.4分布运算符
11.5递归定义
11.6继承
11.7对象包含
11.8多态性
11.9类合并
11.9.1定义类合并
11.9.2多态核心
11.9.3实例：电动工具
11.9.4类合并与多态运算符的区别
11.10self常量
11.11Object—Z语言的工具支持
11.12Object—Z实例研究：银行系统
小结
习题
第12章形式方法及其工具
12.1Z规格说明语言支撑工具
12.1.12／EVES
12.1.2CADiZ
12.1.3ZTC工具
12.1.4ZUserStudio
12.1.5Zeus—Z工具
12.1.6ZtoolsforWord
12.1.72规格说明的动画工具
12.1.8CZT项目
12.1.9其他Z支撑工具
12.2其他形式方法工具
12.2.1PVS
12.2.2Isabelle
12.2.3SPIN
12.2.4SMV
12.2.5Alloy模型分析器
12.3其他形式方法及规格说明语言
12.3.1B方法
12.3.2Event—B方法
12.3.3维也纳开发方法
12.3.4TCOZ语言
12.3.5LO了OS语言
12.3.6Larch语言
12.3.7通信顺序进程
12.3.8时段演算
12.3.9UTP理论
12.3.10SOFL方法
12.3.11TLA+
12.3.12Petri网
小结
习题
附录AZ语法
附录BZ语言术语
附录CObject—Z语法
C.1表示法
C.2缩写
C.3产生式
附录D部分习题解答
参考文献