文 欣

（厦门工学院计算机科学与工程系，厦门 361021）

1 引言

Z是一种形式化规格说明语言，具有严谨、准确的特点，主要应用航空航天、军事等无法重复测试的关键系统领域。但是Z不是一种可执行级语言，因此提出了Z语言向高级语言（C++）自动求精，从而实现从需求说明到编码的自动化。

模式是组成Z语言的基本单位，它分为说明部分和谓词部分，说明部分定义一些状态或模式变量，谓词部分一般是谓词公式。以教师工资系统为例，假设教师姓名定义为TSName，教师工资定义为TSSalary。定义教师名和工资的类型分别为Name和Salary，操作后系统给出的提示信息是：Report：=ok|already exit。初始化模式为InitSalary，形式如下：

模式中的name、salary后跟着一个“?”代表输入变量，Report后跟一个”!”代表输出变量。P Name、P Salary是Z的幂集类型，初始时系统没有任何教师及工资记录，因此谓词部分定义为空。

2 Z到C++的数据求精和过程求精

C++STL模板提供了大量数据结构的算法，不仅支持对容器的操作，还支持用户自己定义的数据类型。Z到C++的求精主要包括数据类型求精和过程求精。

Z的整数类型直接转成C++中的int或long类型，如n1，n2，…，nmZ，转成C++表示为：int n1，n2，… nm.。Z中给定集合可用通用模板结构对类型进行求精，如变量elem：Book，转成C++的代码如下：template＜Book＞Book elem。Z的幂集类型可用C++中的set容器来转换，如上模式的TSName：P Name转C++代码为：set＜Name＞TSName。关系类型如R A←→B在C++中的可表示为：set＜pair＜A，B＞＞R。序列类型用vector容器表示，如Z的序列X seq TypeName可转为：vector＜TypeName＞X。Z的包类型如X bag TypeName可表示为map＜TypeName，count＞，其中count表示每个元素在出现的次数。

Z的过程求精主要是对集合类型的一些常用操作，如集合中增加元素，删除元素、判断元素是否在集合中，集合的交集、并集、补集，集合的子集操作等。下表主要给出集合中一些基本操作求精结果：

集合操作转C++代码

3 Z模式求精实例

以教师工资系统为例，增加教师工资模式为AddSalary，该模式中会涉及到初始模式，使用符号“Δ”表示模式的包含，系统中教师工资变为原来的集合加入新增加的模式，该模式描述如下：

删除教师工资模式为DeleteSalary，当要删除的教师名字时工资也应一起删除，此模式涉及到增加教师工资模式，该模式描述如下：

应用C++STL技术将上述模式转成C++语言，不管是增加教师工资还是删除教师工资，首先都要判断该教师是否在系统中，函数模板如下：

isMember（）方法是判断教师是否在教师工资系统中，使用fi nd方法从头到尾进行查找，如果找到该教师已经在系统中返回真，否则返回假。

addSalary方法功能是插入教师工资，使用insert（）方法进行插入

4 结束语

Z说明向C++语言的自动求精是一个极其复杂的过程，想要Z应用在整个软件开发周期还存在许多问题，如怎样建立一个合理正确的Z模式对大多数开发人员还存在一定难度，Z的过程求精还有一些问题需要改进。如果Z向C++能够完全自动化将对未来的软件开发有着重大意义。