科学出版社2015年6月，ISBN 978-7-03-044787-6。

Z语言是软件工程中对软件的需求、功能、规格进行精确无误并且可以推理和证明的描述语言，它将事物的状态和行为用数学符号来形式化地进行表达，为编写计算机程序和验证计算机程序的正确性提供逻辑和理论依据。所以，Z语言是软件工程中编码之前的规格说明语言。本书是根据作者自20世纪90年代初至今在国内外高校所从事的软件工程教学和科研工作的经验，结合在我国载人航天和深空探测工程中三维可视化系统的设计、研发、使用过程中的体会，针对软件工程中的形式描述这一环节编写而成。书中的第1章至第7章包括了Z语言的基本数学概念、集合、命题、模式、函数、谓词、关系等内容；第8章介绍了使用Z语言的简单实例；第9章介绍了常用的Z语言描述工具及其使用方法；第10章是关于生成Z语言形式描述文档的一个工具及说明。书中的内容以最简单的语言进行表达，并且对大量的数学概念和专业技术进行了通俗地说明。 本书适合做初学者的Z语言教材和软件工程技术人员以及管理人员的参考工具书。

http://www.abook.cn/showproduct.asp?id=5453