形式语言B与OOZS的比较
摘要：介绍了形式化方法B方法和OOZS方法，从软件开发的角度对二者进行了比较，归纳了异同和各自适用范围。
OOZS语言目前尚缺乏严格的形式理论基础，使得OOZS语言的自动推理工具和验证工具的开发尚缺乏坚实的基础。
B方法中的精华和实现是很多形式化开发方法所没有的，他在规格说明的基础上可直接生成可执行系统，并在整个开发过程中通过正确性验证，保证了软件产品的高可靠性、可移植性和可维护性，有效地提高软件的生产率。
毕业论文网 关键词：B；OOZS；形式化方法；比较 中图分类号：G642文献标志码：A文章编号：1673—291X（2011）01—0294—02 引言 形式化方法是软件工程研究的一个重要方面，它是实现软件自动化的基础。
B方法和OOZS同属于软件形式规格说明语言，在一定范围内得到应用。
一、B与OOZS简介 OOZS规格说明语言，是一种结构化的面向对象形式规格说明语言，在规格说明中引入类的概念和继承等面向对象机制，通过提高形式规格说明语言的模块化能力和层次性来改进形式规格说明的清晰度。
OOZS支持大型软件系统的分析及其规格说明的书写，并使之能直接在计算机中进行处理。
B是目前国际上最受重视的实用性软件形式化方法之一，B语言是由Z语言发展而来的，其目的是为这种形式化方法增强模块能力和工具支持能力。
B语言称为一种广谱语言和方法，它既包括高度抽象的数学描述，又包括了可执行的描述。
B语言支持规格说明，并且支持继规格说明之后所有的精化和设计步骤。
B语言是一种支持从规格说明到代码生成整个开发过程的形式化方法。
它使用相对简单且为人们所熟悉的集合符号表示法来描述抽象机的状态变换，从抽象机开始，逐步细化，直到最后的实现程序。
B语言属于基于模型的规格说明符号语言范畴，它构造了一个具有所需特性的特殊数学类型。
二、B与OOZS的异同点 1.B方法符号与OOZS语言符号对照表。
用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术，这样的形式化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻划、开发和验证系统。
如果一个方法有良好的数学基础，那么它就是形式化的，典型地以形式化规约语言给出。
这个基础提供一系列精确定义的概念，如：一致性和完整性，以及定义规范的实现和正确性。
形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。
不同的形式化方法的数学基础是不同的，有些方法是基于集合论和一阶谓词演算。
有些是基于时态逻辑。
OOZS和B就是采用一阶谓词逻辑和集合论作为其形式语义基础，把映射、函数等数学概念用到规格说明中来，简明直观，易于阅读提供了较强的功能描述设施，使用户可以用书写完整的软件规格说明。
3.逻辑基础。
B建立在Zermelo—Frankel集合理论基础上，B抽象机符号表示形式化方法（B AMN）以谓词逻辑、表示集合的符号、序列、函数以及其他抽象数据类型为基础，以一种精确的方法来描述软件系统的需求与设计。
AMN用广义代换语言（Generalised Substitution Language，GSL）的术语定义，B AMN使用经典二值逻辑（真和假）。
OOZS语言基本上采用Z.S语言的记号，对Z语言的符号和框架进行了结构化处理，并基于模块功能的不同，将描述系统结构特征的状态模式和所有作用在该状态模式上的操作模式结合成一个抽象数据类型，从而增加了规格说明中类的描述机制。
此外，OOZS语言还吸收了VDM等语言的一些特征，对操作模型进行了一系列改进。
4.前置条件与后置条件的表示。
B语言的前置条件用Pre表示，后置条件是通过谓词逻辑基础的转换实现的，没有明确给出。
B方法规格说明一般结构如下： MACHINE VARIABLES M（X，x） INVARIANT SETS INITALIZATION S，T={a，b} ASSERATIONS CONSTANTS OPERATIONS PROERTIES END 在OOZS语言操作模式中，谓词部分被划分成Pre谓词和Post谓词，其中，Pre谓词是对操作前的状态描述，表示操作所需要的前置条件；Post谓词是对操作后的状态描述，操作模式操作后所满足的后置条件。
OOZS语言操作模式的形式如下： 〈操作模式〉∷=schema〈标识符〉 [(〈入口形参表〉)] [= =>(〈出口参数表〉)]； 〈声明部分〉； [pre 〈谓词部分〉；] [post 〈谓词部分〉；] End schema 5.多态性和继承性。
面向对象方法的基本特性主要有：多态性、继承性和封装性。
OOZS规格说明的主体由一系列的类组成，这些类之间可以具有聚集或继承关系。
在OOZS规格说明中，用户可以定义“类”，而且“类”可以作为类型来使用。
一个“类”描述了目标系统的一个部分，类之间可以具有继承关系或实例包含关系。
OOZS语言中，类可以带有模板参数，模板参数在类的定义中作为类型使用；超类表声明了类的超类，OOZS语言支持多重继承机制，超类可以是普通类，也可以是模板类。
B抽象机中没有继承性。
6.生命周期的覆盖。
目前，OOZS语言的语法分析程序和类型检查工具已经开发完成，可以自动对OOZS规格说明进行语法检查和类型检查。
但是，作为一种规格说明语言，OOZS语言目前尚缺乏严格的形式理论基础，这使得OOZS语言的自动推理工具和验证工具的开发尚缺乏坚实的基础。
结束语 通过对OOZS和B语言的比较，得知不同形式规格说明语言有各自的特点及适用范围。
OOZS语言目前尚缺乏严格的形式理论基础，使得OOZS语言的自动推理工具和验证工具的开发尚缺乏坚实的基础。
B方法中的精华和实现是很多形式化开发方法所没有的，他在规格说明的基础上可直接生成可执行系统，并在整个开发过程中通过正确性验证，保证了软件产品的高可靠性、可移植性和可维护性，有效地提高软件的生产率。
参考文献： [1]B方法[M].裘宗燕，译.北京:电子工业出版社，2004:6. [2]邹盛荣，郭忠伟，彭昱静，周塔，顾爱华，卫丽.形式化B方法到UML类图的转化研究及应用[J].计算机时代，2009，(3). [3]朱志勇.面向对象软件形式开发方法[J].湖南科技学院学报，2005，(11):209—211.[责任编辑 陈鹤]。