缪淮扣、陈怡海编写的《软件形式规格说明语言—Z》是普通高等教育“十一五”国家级规划教材。教材共分第12章，内容包括：绪论，一阶逻辑与集合论，Z的类型与构造单元，关系和函数，模式和规格说明，序列和包，规格说明的实例，Z规格说明的形式推理，Z规格说明的若干推理实例，从规格说明到程序，Object—Z规格说明语言，形式方法及其工具。

本书各章都配有习题。附录A给出了Z的语法；附录B给出了Object—Z的语法；附录C给出了部分习题解答。

形式方法是一种基于数学的软件开发方法。形式规格说明是形式方法最基本的部分，它精确描述用户需求和计算机软件系统的功能，并用于软件验证和精化。Z是目前颇受欢迎且使用较广泛的一种形式规格说明语言。缪淮扣、陈怡海编写的《软件形式规格说明语言—Z》旨在讨论软件工程中形式方法的概念、方法和表示法，并详细介绍Z的类型系统、数学语言和公理定义、通用式定义、模式等结构，还讨论了Z规格说明的推理和求精方法。《软件形式规格说明语言—Z》还介绍了面向对象的规格说明语言Object—Z和其他形式方法表示和工具。全书结构合理、内容丰富、实例详尽多样。各章配有习题。

《软件形式规格说明语言—Z》可作为计算机、软件工程、信息安全和信息管理等专业本科生和研究生的教材，也可作为大专院校有关专业的教师参考书，还可作为从事软件工程、软件开发和软件应用的研究人员和技术人员的参考资料。

第1章 绪论

第2章 一阶逻辑与集合论

第3章 Z的类型与构造单元

第4章 关系和函数

第5章 模式和规格说明

第6章 序列和包

第7章 规格说明的实例

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

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

第10章 从规格说明到程序

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

第12章 形式方法及其工具

附录A Z语法

附录B Z语言术语

附录C Object—Z语法

附录D 部分习题解答

参考文献