[敬请读者注意] 本人保留本文的全部著作权利。如果哪位读者使用本文所描述内容，请务必如实引用并明白注明本文出处。如果本人发现任何人擅自使用本文任何部分内容而不明白注明出处，恕本人在网上广泛公布侵权者姓名。敬请各位读者注意，谢谢！

形式化规格描述语言Z 

程京德

    “软件工程”是为了保证大规模软件系统的高可靠性，研究以系统化的、规范化的、可量化的、过程化的工程方法去定义、设计、开发和维护大规模软件系统，以及如何将这些方法应用到工程实践的工程专业学科[1]。

    由美国联邦航空管理局(FAA)及国家航空和宇宙航行局(NASA)联合发布的一份调查报告中阐述道：“形式化方法应该是每个计算机科学家和软件工程师教育的一部分，正如应用数学的适当分支是所有其他工程师教育的必要部分一样(Formal methods should be part of the education of every computer scientist and software engineer, just as the appropriate branch of applied mathematics is a necessary part of the education of all other engineers)”[1]。

    法国计算机科学家 Jean-Raymond Abrial 最早在1974年使用了形式化的表记法[2]，在1977年提出了形式化规格描述语言 Z 的早期版[3,4]。在 Abrial 于1979年进入牛津大学程序设计研究组之后，Z 得到了进一步发展。名称“Z”是为了寓意其基于 Zermelo-Fraenkel公理集合论。

    作为形式化规格描述语言，Z 具有如下特征：

    （1）Z 以 Zermelo-Fraenkel公理集合论和经典一阶谓词演算为基础；用集合来定义各种类型，用一阶谓词逻辑式来表达各种操作应该满足的性质。

    （2）Z 是强类型化的规格描述语言，亦即，任何被描述的数据对象都必须有其类型。

    （3）Z 是基于状态的规格描述语言，亦即，使用状态转移概念来描述对象系统的行为，对系统的操作是通过描述它们的执行如何改变系统状态来指定的。

    （4）Z 支持表达抽象（通过定义变量及其类型、全局常量、状态空间）和操作抽象（通过定义操作及其应该满足的性质）。

    （5）Z 定义了“schema”结构化表达，以 schema 演算提供对规格描述的结构化手段，极其方便于描述大规模对象系统。

    （6）Z 没有引入“赋值”概念，因此 Z 的规格描述是非过程化的，用等式来静态地表达状态转移前后变量之间关系，没有因为对变量赋值而引起的副作用。

    （7）Z 没有引入清晰地表达并发性的手段。

    下图显示了 schema 的一般结构：    

    一个 schema 一般由 schema 名称、定义、和谓词三个部分构成。schema 名称被用来参照和参与 schema演算，定义部分定义以该 schema 为辖域的局部变量，并且可以通过 schema算子来引入已经定义过的其它 schema，谓词部分规定该 schema 中局部变量以及通过 schema算子引入的变量之间必须满足的性质（约束）。

    可以通过省略 schema 名称的 schema 来定义以整个规格描述为辖域的全局变量。  

    下图显示一个 Z 规格描述（The X Window System 规格描述）[5] 中的 schema 实例；

    在上例中，X 是一个已经定义过的 schema，通过德尔塔schema算子引入到 schema CreateWindow 中，parent? 是具有类型 Window 的局部输入变量，bgnd? 是具有类型 Pixmap 的局部输入变量，w! 是具有类型 Window 的局部输出变量。谓词部分中的变量 windows、order、mapped 是通过德尔塔schema算子引入的既定义 schema X 中定义的变量。

    2002年，国际标准化组织颁布了形式化规格描述语言 Z 的国际标准：International Standard ISO/IEC 13568, Information technology - Z formal specification notation — Syntax, type system and semantics, 2002-07-01。

    本文为笔者多年来讲授“软件工程形式化方法”课程中对学生们介绍形式化规格描述语言 Z 之内容的拔萃，提供给有兴趣的读者参考。

参考文献

[1] 程京德,“为什么软件工程师必须知道形式化方法？” 微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年9月26日。

[2] J.-R. Abrial, “Data Semantics,” in J. W. Klimbie and K. L. Koffeman (eds.), Proceedings of the IFIP Working Conference on Data Base Management, pp. 1-59, North-Holland, 1974.

[3] J.-R. Abrial, S. A. Schuman, and B. Meyer, “A Specification Language,” in A. M. Macnaghten and R. M. McKeag  (eds.), “On the Construction of Programs,” Cambridge University Press, 1980. 

[4] B. Meyer, “On Formalism in Specifications,” IEEE-Software, No. 2, pp. 6-26, 1985. 

[5] J. P. Bowen, “Formal Specification and Documentation Using Z: A Case Study Approach,” International Thomson Computer Press 1996, Revised 2003.

微信公众号“数理逻辑与哲学逻辑”