软件形成化方法与软件规格说明语言—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 形式规格说明语言Z

1.4.1 Z语言概述

1.4.2 Z规格说明简例

小结

习题

第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.1 Z的类型系统

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.3 Z的基本库

3.3 Z规格说明的构造单元

3.3.1 Z的符号

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章 模式和规格说明

第6章 序列和包

第7章 规格说明的实例

第8章 Z规格说明的形式推理

第9章 Z规格说明的若干推理实例

第10章 从规格说明到程序

第11章 Object-Z规格说明语言

第12章 形式方法及其工具

附录A Z语法

附录B Z语言术语

附录C Object-Z语法

附录D 部分习题解答

参考文献

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

《普通高等教育“十一五”国家级规划教材·软件工程专业核心课程系列教材：软件形式规格说明语言Z》具有以下特点：
1 教育部高等学校软件工程专业教学指导分委员会推荐教材。
2 根据教育部“软件工程课程体系研究”项目成果《中国软件工程学科教程》及专业规范组织编写。
3 与最新ACM和IEEE CCSE同步。
4 汇集示范性软件工程专业教学成果。