中国电子科学研究院学报稿件信息
基于C++STL技术实现Z模式自动求精的研究
文欣
（厦门工学院计算机科学与工程系，厦门361021）
摘要：Z语言是以一阶谓词和集合论为基础的一种形式化规格说明语言, 目前主要应用在软件开发周期的需求阶段和测试阶段。本文主要研究的是基于STL技术实现Z模式向高级语言C++的自动求精，以达到提高软件开发的效率。
关键词：C++STL; Z规格说明; 模式
Research on Z Model Automatic Refining Based on C++ STL Technology
Wen Xin
(Department of Computer Science and Engineering, Xiamen Institute of Technology,Xiamen 361021)
Abstract：Z specification language is based on first-order predicates and set theory. One is the formal language, the requirements stage and test stage of the main application software. This article mainly introduces the implementation of Z mode to advanced language C++ based on C++ STL technology. Automatic refinement, To improve the efficiency of software development.
Key words:C++STL;Z specification language; model
一.引言
Z 是目前比较流行的一种形式化规格说明语言，它以一阶谓词逻辑和集合论为基础，具有严谨、简明、精确的特点。Z语言非常适用于航空航天、军事、银行等无法重复测试的关键系统领域。Z规格说明不是一种可执行级语言，不能应用在软件开发的各个阶段，因此在工业界的发展比较缓慢，鉴于上述原因提出了Z规格说明向高级语言（C++）自动求精，从而实现从需求说明到编码的自动转化。
Z语言描述的是“做什么”，不是“怎么做”，它没有高级语言的顺序、选择、循环语句。模式是组成Z语言的基本单位，它分为说明部分和谓词部分，说明部分定义一些状态或模式变量，谓词部分一般是谓词公式。模式分为状态模式和操作模式2类：
状态模式：描述目标软件系统某一部分数据类型结构特征的模式，称为状态模式。通常一个模式描述系统的状态，实际上是指描述了系统的数据的状态。
操作模式：描述的是操作执行前后系统某部分状态值之间的关系，定义了与若干个状态模式相关的该部分行为。Z规格说明中，不论是状态模式还是操作模式，一般用垂直形式如下表示。
我们现在通过一个具体例子来说明Z模式书写过程。本文以教师工资系统为例，假设系统中教师的姓名定义为TSName，教师的工资定义为TSSalary。定义教师名和工资的类型分别为Name和Salary，定义操作之后系统给出的提示信息是： Report：：=ok|already exit。定义该初始化模式为InitSalary。
在定义模式过程中，需要用某种方式区别输入和输出变量、前状态变量和后状态变量。Z输入变量采用的是输入变量的最后一个字符跟着一个“?”,如上的name和salary，它们分别为输入变量。Z的输出变量是最后一个字符紧跟一个”!”，如上的Report。P Name、P Salary是Z的数据类型，代表幂集，初始时系统没有任何教师及工资记录，于是谓词部分定义为空。我们还可以定义增加教师工资、删除教师工资等模式，将在后面列举出来。
二．Z到C++STL的数据求精和过程求精
C++ STL（标准模板库）是一套功能强大的 C++模板类，提供了通用的模板类和函数，这些模板类和函数可以实现多种流行和常用的算法和数据结构，如向量、链表、队列、栈。
STL由迭代器、算法、容器、函数对象和内存分配器五大部分组成。容器主要分为2大类：序列式容器和关联式容器。序列式容器主要有vector、list和deque。关联式容器有set、map。
STL提供了大量的数据结构的算法，不仅支持对容器的操作，还支持用户自己定义的数据类型。迭代器类似C++中的指针，可以非常快速对STL的内容进行访问。
本文主要研究的是通过C++ STL提供的这些组件和算法把Z语言转成C++语言，从而达到可执行的高级语言。Z到C++的求精主要包括数据类型求精和过程求精。Z的数据类型的求精比较简单，基本上完全可以实现，过程类型的求精在这里只完成了一部分。
Z的整数类型直接转成C++中的int或者long类型 ,如n1,n2,…,nm Z， 转成C++表示为：int n1,n2,… nm.。Z的枚举类型转成C++的形式为：enum TypeName{enum1,enum2,enum3,…enumn},其中TypeName是枚举类型名，enum1,enum2,enum3,…enumn是枚举类型标志符。Z的给定集合可以使用通用模板结构对类型进行求精，比如给定类型Book,数据类型变量elem:Book,转成C++的代码如下：template <Book> Book elem。Z中集合称为幂集类型，它可以使用C++中的set容器来转换，比如TSName：P Name 转成C++代码形式为：set<Name> TSName。笛卡尔积是一个有序的元组，它可以用C++中的struct关键字来定义，如有笛卡尔积类型变量 Ident n1×n2×n3×…×nm,可以表示为：
struct{
n1 a1;
n2 a2;
…
nm am;
}Ident
关系和函数是笛卡尔积的一种特例，如有关系：R A 
B 在C++中的表示为：set<pair<A,B>>R,其中pair容器为STL中用struct 定义的二元组容器。序列可以转成用vector容器表示，如Z的序列X seq TypeName 可表示为：vector<TypeName> X。Z的包类型如 X bag TypeName可表示为map<TypeName,count>,其中count表示每个元素在出现的次数。
Z的过程求精本文主要是对集合类型的一些常用操作，例如集合中增加元素，删除元素、判断元素是否在集合中，集合的交集、并集、补集，集合的子集操作等。下表主要给出集合的一些基本操作求精的结果：
集合操作转C++代码
|
操作类型 |
Z规格说明 |
C++STL代码 |
|
集合交集运算 |
M ∩ N |
set<T> intersection(set<T> M,set<T> N) |
|
集合并集运算 |
M ∪ N |
set<T> union(set<T> M,set<T> N) |
|
集合补运算 |
M \ N |
set<T> difference(set<T> M,set<T> N) |
|
元素属于运算 |
a |
bool isMember(T a,set<T> M) |
|
删除元素运算 |
|
int delete(T oElement) |
|
增加元素运算 |
|
int insert(T newElement) |
|
集合子集运算 |
M |
bool isSubset(set<T> M,set<T> N) |
三.Z模式求精实例
以教师工资系统为例，初始化模式InitSalary上面已经完成,增加教师工资模式名为AddSalary,该模式涉及到初始模式，使用符号”r”表示模式的包含，系统中的教师工资变为原来的集合加入新增加的模式，该模式描述如下：
当我们删除教师工资时，输入要删除的教师名字，然后将对应的教师工资一起删除，此模式涉及到增加教师工资模式，形式如下：
应用C++STL技术将上述模式转成C++语言，不管是增加教师工资还是删除教师工资，我们都要判断该教师是否在系统中，具体函数模板如下：
#incliude<set>
bool isMember(set<Name> _zset, Name elem){
set<Name>::iterator _iterator;
_iterator=find(_zset.begin(),_zset.end(),elem);
if(_iterator==_zset.end()){
return false;}
else{
return true;}
isMember()方法是判断教师是否在教师工资系统中，我们使用 find方法从头到尾进行查找，如果找到该教师已经在系统中返回真，否则返回假。
int addSalary(set<Name> _zset,Name elem){
_zset.insert(elem);//使用insert()方法进行插入
}
int deleteSalary(set<Name> _zset,Name elem){
_zset.delete(elem)//使用delete()方法进行删除
}
C++主程序算法如下：
#include<set>
int main(){
set<Name> _setName;
set<Salary> _setSalary;
Name _name;
cin>>_name;
if(isMember(_setName,_name)){
deleteSalary(_setName,_name);
}
else{
addSalary(_setName,_name); }
}
四.结论：
Z规格说明向C++语言的自动求精是一个极其复杂的过程，Z语言是一个以数学为基础的描述语言，具有严谨、晦涩难懂的特点，它主要用于软件的开发阶段和测试阶段。想要Z应用在整个软件周期还存在许多问题，如怎样建立一个合理正确的Z模式对大多数开发人员还存在一定难度，Z数据类型求精基本完成，Z的过程求精还有一些问题需要改进。如果Z向C++转化能够完全自动化将对未来的软件开发有着重大意义。
参考文献：
[1] 缪淮扣,李刚.软件工程语言—Z.上海：上海科学技术文献出版社,1999.
[2] 王宏生,王晓龙,李巍巍.基于C++STL的Z规格说明数据类型的表示[J].沈阳:辽宁大学学报,自然科学版,2005，（1）：59-62.
[3] 王昕译.C++STL中文版[M].北京: 中国电力出版社,2002:265-284
[4] 高晓雷, 缪淮扣,李勇.jiyu C++模板的Z规格说明的数据类型的实现[J].上海:计算机工程,第11期,2006,(6):45-48.
[5] Diller.Z An Introuduce to Formal Method[M],Load-on:John Wiley,1990:186-212.
