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

软件工程中的形式方法是一种基于数学的软件开发方法，它可应用于软件工程的各个阶段。用形式方法开发软件可提高软件系统的正确性和可靠性，并可提高软件开发的效率。该方法日益受到计算机界和工业界的高度重视，并得到越来越广泛的应用。著名的欧洲 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 版本提供的浮点运算支持。 多年来，美国、加...