形式化语言B与UML/OCL的比较

顾建丰, 陈名铭, 周秀芳

摘要:该文介绍了形式化方法中B语言和UML/OCL语言,从软件开发生命周期的角度对B语言和OCL语言进行了比较,归纳了这两种形式化语言的异同和各自的适用范围。

关键词:B语言;OCL;形式化方法;比较

中图分类号:TP311文献标识码:A文章编号:1009-3044(2009)34-9739-03

Formal Language B and UML/OCL Comparison

GU Jian-feng1,2, CHEN Ming-ming1, ZHOU Xiu-fang3

(1. College of Information Engineering, Yangzhou University, Yangzhou 225009, China; 2. Jiangsu TV University Wujin College, Changzhou 213149, China)

Abstract: This article introduced in the formalized method the B method and the UML/OCL language. Has carried on the comparison from the softwaredevelopment life cycle's angle to the B language and OCL, has induced these two kind of formalized language similarities and differences and therespective applicable scope.

Key words: B language; OCL; Formalized method; Compare

软件开发的全过程中,从需求分析、规格说明、设计、编程、系统集成、测试、文档生成直至维护各阶段,凡是采用严格的数学语言、具有精确的数学语义的方法都称为形式化方法[1]。统一建模语言UML与形式化方法的结合是近年来的研究热点[2],统一模型语言UML在软件开发过程中已有很多的实践应用,一种形式化语言OCL(对象约束语言)[3]的引入可以提高UML模型的精确性,B语言是一种基于对象的形式化语言。

1 UML/OCL与B的简介

UML(Unified Modeling Language统一建模语言)是一种定义良好,易于表达,功能强大,且普遍适用的建模语言。它采用直观的图形表示法对系统建模,统一模型语言UML在软件开发过程中已有很多的实践应用,已在面向对象分析和设计中成为事实上的工业标准,是现今面向对象需求分析的重要工具。但UML缺乏对软件模型的精确描述,OCL的引入可以提高UML模型的精确性,弥补了UML的不足,它是一种精确的、易于使用的形式化语言,避免了其他形式化语言中那些复杂的约束符号,由其约束的UML模型不会发生语义二义性问题,OCL是一种形式化语言。B方法属于基于模型的规格说明语言的范畴,也是一种基于对象的形式化语言。

2 B和OCL的比较

2.1 数学基础

用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术[3],这样的形式化方法提供了一个框架,可以在框架中以系统的而不是特别的方式刻划、开发和验证系统。如果一个方法有良好的数学基础,那么它就是形式化的,典型地以形式化规约语言给出。这个基础提供一系列精确定义的概念,如:一致性和完整性,以及定义规范的实现和正确性。

所有形式规格说明方法都是以数学为基础的。有些方法是基于集合论和一阶谓词演算,有些方法是基于时态逻辑,OCL语言是基于集合论和三值Kleene逻辑。B语言是基于集合论和一阶谓词演算。

2.2 逻辑基础

B建立在Zermelo-Frankel集合理论基础上,B抽象机符号表示形式化方法(B AMN)以谓词逻辑、表示集合的符号、序列、函数以及其它抽象数据类型为基础,以一种精确的方法来描述软件系统的需求与设计。AMN用广义代换语言(Generalised Substitution Language, GSL)的术语定义,B AMN使用经典二值逻辑(真和假)。OCL语言是基于三值逻辑(True,False,Undefined)。

2.3 书写风格

B建立在规格说明的谓词转换器的风格上,在使用前置/后置条件的地方,用替换来表明状态的改变。如:

B:insert(elem)=

PRE

elem:TYPE &

elem/:var

THEN

Var:=var∨{elem}

END

B中的后置条件象一个赋值,因而使得规格说明看起来像伪程序,其实它的语义恰如状态的替换。

OCL语言使用了大量的关键字(如self,context,pre,post等),其风格类似于编程语言。

2.4 表达能力

从表达能力来分析,B语言的表达能力比OCL语言更强,OCL语言只能对模型的约束加以说明,使用B方法编写的规格说明具有精确性、无二义性、一致性、能进行推理等特点。

OCL语言是一种半形式化的语言,正式的OCL1.5版本的规格说明中尽管对OCL语言的语法进行了详细的描述,但是没有对其形式语义进行过定义,而最新的OCL2.0版本的草案中提出了两种语义,一种是基于元模型的语义,另一种是称之为对象模型的集合论的形式语义已有研究人员指出这两种语 义 存在着不一致性和不完备性。

2.5 前置条件、后置条件明确性

一个操作的前置条件是指在操作被执行前必须为真的约束,一个操作的后置条件是指在操作执行完成后必须为真的约束。在B语言中,前置条件是明确陈述的,冗余的前置条件需要一致性检测,OCL的前置条件也是明确给出的,用关键字Pre表示。在B中,不变式是冗余的,不变式的存在与否都不会改变操作的定义,它并不是操作后置条件的一部分,因而需要证明该操作是否必须保留不变式,而在OCL中,后置条件也明确给出了,用关键字Post表示。

2.6 工具支持

一种规格说明语言要得到广泛的应用,强有力的工具支持是至关重要的。一般而言,规格说明语言的支持工具可以分为下面几种类型:

1)可视化编辑工具:主要是用于对规格说明语言进行输入和编辑。

2)语法检查工具:是规格说明语言最基本的支持工具,其功能是用于检查规格说明的语法正确性,但这种工具只能发现一些简单的语法错误。

3)类型检查工具规格说明语言均为类型语言使用类型检查工具的目的是为了保证规格说明类型的正确性。

4)语义分析工具:是用来检查规格说明的语义的正确性。

5)规格说明的求精:求精是指将规格说明转换到程序代码。

6)测试自动化工具:测试自动化是指从规格说明中产生测试用例,运行测试用例和进行测试结果分析的自动化,这些工具能提高软件开发的效率并且降低软件维护费用。

7)验证和确认工具:主要是用于对规格说明进行验证和确认,以保证规格说明具有所需要的性质。验证和确认方式主要有模型检查,定理证明和动画技术三种。

OCL语言是一种相对较新的语言,因此目前该语言还没有足够的支持工具。大多数商业化的UML建模工具并没有普遍提供对OCL语言的支持,只有一些研究人员对OCL的语义和支持工具进行过研究。其相应工作介绍如下:

1)OCL编辑工具目前主流的UML编辑工具如ArgoUML和MagicDraw等都提供了对OCL语言的支持,并提供了XMI格式的输出。

2)词法分析和类型检查工具 首先出现的OCL支持工具是IBM公司出品的OCL词法分析器,它是用Java和JavaCC词法产生器编写的。该分析器的功能包括语法分析和部分的类型检查。后来出现的OCL词法分析器偶Klasse Objecten公司出品的OCL词法分析器,但它只能提供词法分析。ArgoUML工具中集成了Dresden提供的OCL编译器,它能提供完整的OCL语法和类型检查。在MagicDraw工具中也可以对OCL语法进行检查。

3)其他OCL语言支持工具Bremen大学开发了USE(UML-based Specification Environment)系统工具。USE是一种用于信息系统规格说明的验证确认工具。USE能对系统的模型进行动画并规格说明和用OCL语言表达的非形式需求进行确认,在对系统模型进行动画的过程中用户可以创建并操纵系统状态。

B因为有工具支持而获得相当大的优势,像B-Toolkit这种高质量的商业软件有一套完整的开发过程的支持用来完成如下一些任务:类型检测、动画、证明法则生成、交互或自动的证明支持、代码翻译、文档以及带有配置管理功能的综合开发环境支持。

2.7 生命周期的覆盖

B支持从规格说明描述到详细设计的软件开发全过程,而OCL语言只能对系统模型的约束进行说明,不能支持从规格说明的描述到详细设计的软件开发全过程。

3 实例分析

为了更好地展示两种语言的特性,举一个班级人数的实例,例如对于一个班级而言,只有注册人数大于25人方可开课,并且由于教室大小的约束,人数又不能超过80人。我们来分别讨论两种形式化语言的规格说明:

3.1OCL规格说明

首先考虑如何对类的不变式进行说明使用可以对班级人数的属性加上如下的约束:

班级的学生人数必须大于25人并且小于80人。

Context Class

Inv:self.numberofstudents>=25 and self.numberofstudents<=80

每个学生必须经注册后方能听课

Context Student

Inv:self.isRegistered=true

对于操作而言,可以通过前置条件与后置条件加以辅助说明

Context Class::register(p:student)

Pre registerPre:class->excludes(p)

Post registerPost:class->includes(p)

上述的规格说明表示当学生完成注册以后学生成为班级的成员。

3.2 B规格说明

MACHINE student

SETS STUDENT

VARIABLES s, number

INVARIANT

s student∧

number∈NAT

OPERATIONS

s ← register(st) =

PRE

student≠STUDENT∧ n∈NAT

THEN

ANY st WHEREst∈STUDENT - student

THEN

studnet:=student∪{st}‖

s:=st

END

4 结束语

通过对B语言和OCL语言的比较,可以知道不同形式规格说明语言有各自的特点及适用范围。OCL语言是一种文本性规格说明语言,但是没有传统形式语言的复杂性。作为UML标准的一部分,OCL被建模者用来说明UML的约束,如不变式、操作的前置、后置条件、状态门限和属性派生规则等,这大大增加了UML模型描述的精确性。然而,要使OCL表达式的解释没有二义性,必须给出OCL表达式语义的精确定义。OCL表达式语义描述有两种可替换定义方法,使用UML元模型的标准描述形式和使用形式化的非标准描述形。B方法中的精化和实现是很多形式化开发方法所没有的,它在规格说明的基础上可直接生成可执行系统,并在整个开发过程中通过正确性验证,保证了软件产品的高可靠性、可移植性和可维护性,从而可有效提高软件的生产率。

参考文献:

[1] 邹盛荣,郑国梁. B语言和方法与Z、VDM的比较[J].计算机科学,2002(10).

[2] 肖健宇,张德运. OCL数据类型到B形式化规约的转换[J]. 计算机工程,2006(3):61-62.

[3] 陈怡海,缪淮扣. OCL与Object-Z作为UML约束语言的分析比较[J]. 计算机科学,2004,31(12):182-183.