软件工程中的形式方法是一种基于数学的软件开发方法，它可应用于软件工程的各个阶段。用形式方法开发软件可提高软件系统的正确性和可靠性，并可提高软件开发的效率。该方法日益受到计算机界和工业界的高度重视，并得到越来越广泛的应用。著名的欧洲 Esprit 项目的Large Correct System、美国 HP 公司的 Analysis Information Library、得克萨斯的 Computational Logic Inc. 开发的 VIPER (Verifiable Integrated Processor for Enhanced Reliability) 等都使用了形式方法。形式方法已成为可信软件开发的重要方法，并得到重视和应用。

软件形式规格说明是形式方法最基本的部分。形式规格说明精确地描述了用户的需求、软件系统的功能和各种性质，它描述的是“做什么”，而不考虑“怎么做”。Z是目前人们比较感兴趣的一种形式规格说明语言。它是由著名计算机科学家 Hoare 所在的牛津大学程序设计研究组(PRG)的学者在20世纪80年代初设计开发的。事实上, Z本身是一种表示法，是一种建立在坚实的数学基础上的基于模型的规格说明方法，在工业界和学术界已有不少应用。最著名的例子是英国 Hursley 的 IBM 公司将Z应用到CICS(Custom Information and Control System)软件系统，获得成功，软件开发费用降低了9%。牛津大学的 PRG 将Z规格说明方法成功地应用于为 Transputer Inmos T800 版本提供的浮点运算支持。

多年来，美国、加拿大、日本、澳大利亚和欧洲的一些国家，尤其是英国，对Z进行了深入的研究和开发。人们还把Z和结构化的分析方法、面向对象的方法以及程序变换等课题结合起来研究。在每年的关于形式方法的国际学术会议上都有关于Z语言及其相关技术的研究工作的报道。在IEEE 有关软件工程的国际学术会议上，也有不少关于Z的研究成果的报道。国内也有一些学者对Z进行研究，并取得了成果。

我们认为，作为计算机专业、软件工程专业和信息管理专业的本科生和研究生应该了解和掌握软件工程中的形式规格说明方法。另外，Z方法的介绍能使读者加深将一阶逻辑和离散数学的知识应用于软件开发实践的理解。国外已有不少关于Z的教材，而在国内并不多见。基于这样的目的，笔者于1999年编写了国内第一本系统介绍Z规格说明语言的教材《软件工程语言——Z》，由中国工程院院士、国防科技大学陈火旺教授主审。本书在该教材的基础上重新编著，对原来的各章做了部分修改。重写了第1章和第10章，增加了第11章和第12章。

全书共分12章，前两章是基本知识，第 1 章介绍了软件工程、形式方法、Z规格说明方法的基本概念，使读者了解形式规格说明方法在软件生命期中的地位、Z规格说明方法的优缺点。第 2 章介绍了一阶逻辑和集合论的知识，包括命题逻辑和谓词逻辑的概念、真值表技术和逻辑公式的证明、集合的表示和运算。

第3~7章是Z表示法的主要内容。第 3 章介绍Z的类型系统和构造单元，包括Z的类型、扩充表示法、Z的符号、公理定义、模式和通用式定义。第 4 章着重介绍Z的数学语言部分：关系和函数，包括关系的表示和操作以及各种特殊函数。第 5 章是关于Z的最主要的结构——模式的介绍，详细叙述了模式的功能、模式修饰和包含、关于模式的各种运算、模式类型和通用模式以及如何书写Z规格说明的方法。第 6 章是关于 Z的两个构造类型，序列和包的专门介绍，叙述了序列和包的表示和各种操作。第 7 章将第 2~6 章的知识综合在一起，以三个不同类型的实例介绍了构造Z规格说明的方法。

最后5章是关于Z方法的进一步研究和讨论，第 8 章介绍了Z规格说明中定理的表示、初始化定理的证明、前置条件的简化、用于序列的结构归纳法和Z规格说明中各种性质的证明方法。第 9 章介绍了若干Z规格说明中的推理实例。第 10 章是关于从规格说明到程序的软件精化方法的讨论，介绍了Z规格说明精化的方法，并给出了求精的示例。第 11 章完整介绍了面向对象的形式规格说明语言ObjectZ。第 12 章介绍了Z的支撑工具、其他形式方法及其规格说明语言和一些支持工具。

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

本书第 1~9 章由缪淮扣编写，第 10~12 章由陈怡海编写，全书由缪淮扣统稿。

　　本书编写过程得到了上海大学教材建设基金的资助和上海市教委第五期重点学科建设项目(编号J50103)的支持；也得到了国家自然科学基金项目(批准号：60970007、61170044)的支持和帮助；在教材的编写过程中，曾红卫教授、刘玲博士、许庆国博士等对教材的编写和修改提出了建议；日本法政大学刘少英教授对其中的关于SOFL方法的介绍提出了修改建议；华东师范大学刘静教授提供了UTP理论的介绍；曹晓夏博士对第10章的编写提出了建议，并对初稿进行了修改；刘玲和曹晓夏等人在课题组攻读博士和硕士学位期间，作为主要完成人参与了Z规格说明语言的支持工具的开发；朱彬、刘辉、冯学勇、马发俊、童翠玲、高如海、王皙和陈超等对习题解答进行了检查和修改；吴云霞承担了较多的录入工作。本书编写还得到了上海大学计算机工程与科学学院许多老师的帮助，在此一并表示感谢。

    在编写本教材的过程中，参考引用了不少文献，特别是国外有关Z的教材。　

    由于作者水平有限，书中难免有不妥之处，殷切希望广大读者批评指正。

作者

2012年6月