程京德
形式化规格描述语言Z
2024-9-30 09:18
阅读:1070

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

   

形式化规格描述语言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.

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

转载本文请联系原作者获取授权,同时请注明本文来自程京德科学网博客。

链接地址:https://wap.sciencenet.cn/blog-2371919-1453303.html?mobile=1

收藏

分享到:

当前推荐数:0
推荐到博客首页
网友评论0 条评论
确定删除指定的回复吗?
确定删除本博文吗?