顧建豐, 陳名銘, 周秀芳

摘要:該文介紹了形式化方法中B語言和UML/OCL語言,從軟件開發(fā)生命周期的角度對(duì)B語言和OCL語言進(jìn)行了比較,歸納了這兩種形式化語言的異同和各自的適用范圍。

關(guān)鍵詞:B語言;OCL;形式化方法;比較

中圖分類號(hào):TP311文獻(xiàn)標(biāo)識(shí)碼:A文章編號(hào):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

軟件開發(fā)的全過程中,從需求分析、規(guī)格說明、設(shè)計(jì)、編程、系統(tǒng)集成、測(cè)試、文檔生成直至維護(hù)各階段,凡是采用嚴(yán)格的數(shù)學(xué)語言、具有精確的數(shù)學(xué)語義的方法都稱為形式化方法[1]。統(tǒng)一建模語言UML與形式化方法的結(jié)合是近年來的研究熱點(diǎn)[2],統(tǒng)一模型語言UML在軟件開發(fā)過程中已有很多的實(shí)踐應(yīng)用,一種形式化語言O(shè)CL(對(duì)象約束語言)[3]的引入可以提高UML模型的精確性,B語言是一種基于對(duì)象的形式化語言。

1 UML/OCL與B的簡(jiǎn)介

UML(Unified Modeling Language統(tǒng)一建模語言)是一種定義良好,易于表達(dá),功能強(qiáng)大,且普遍適用的建模語言。它采用直觀的圖形表示法對(duì)系統(tǒng)建模,統(tǒng)一模型語言UML在軟件開發(fā)過程中已有很多的實(shí)踐應(yīng)用,已在面向?qū)ο蠓治龊驮O(shè)計(jì)中成為事實(shí)上的工業(yè)標(biāo)準(zhǔn),是現(xiàn)今面向?qū)ο笮枨蠓治龅闹匾ぞ摺５玌ML缺乏對(duì)軟件模型的精確描述,OCL的引入可以提高UML模型的精確性,彌補(bǔ)了UML的不足,它是一種精確的、易于使用的形式化語言,避免了其他形式化語言中那些復(fù)雜的約束符號(hào),由其約束的UML模型不會(huì)發(fā)生語義二義性問題,OCL是一種形式化語言。B方法屬于基于模型的規(guī)格說明語言的范疇,也是一種基于對(duì)象的形式化語言。

2 B和OCL的比較

2.1 數(shù)學(xué)基礎(chǔ)

用于開發(fā)計(jì)算機(jī)系統(tǒng)的形式化方法是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)[3],這樣的形式化方法提供了一個(gè)框架,可以在框架中以系統(tǒng)的而不是特別的方式刻劃、開發(fā)和驗(yàn)證系統(tǒng)。如果一個(gè)方法有良好的數(shù)學(xué)基礎(chǔ),那么它就是形式化的,典型地以形式化規(guī)約語言給出。這個(gè)基礎(chǔ)提供一系列精確定義的概念,如:一致性和完整性,以及定義規(guī)范的實(shí)現(xiàn)和正確性。

所有形式規(guī)格說明方法都是以數(shù)學(xué)為基礎(chǔ)的。有些方法是基于集合論和一階謂詞演算,有些方法是基于時(shí)態(tài)邏輯,OCL語言是基于集合論和三值Kleene邏輯。B語言是基于集合論和一階謂詞演算。

2.2 邏輯基礎(chǔ)

B建立在Zermelo-Frankel集合理論基礎(chǔ)上,B抽象機(jī)符號(hào)表示形式化方法(B AMN)以謂詞邏輯、表示集合的符號(hào)、序列、函數(shù)以及其它抽象數(shù)據(jù)類型為基礎(chǔ),以一種精確的方法來描述軟件系統(tǒng)的需求與設(shè)計(jì)。AMN用廣義代換語言(Generalised Substitution Language, GSL)的術(shù)語定義,B AMN使用經(jīng)典二值邏輯(真和假)。OCL語言是基于三值邏輯(True,False,Undefined)。

2.3 書寫風(fēng)格

B建立在規(guī)格說明的謂詞轉(zhuǎn)換器的風(fēng)格上,在使用前置/后置條件的地方,用替換來表明狀態(tài)的改變。如:

B:insert(elem)=

PRE

elem:TYPE &

elem/:var

THEN

Var:=var∨{elem}

END

B中的后置條件象一個(gè)賦值,因而使得規(guī)格說明看起來像偽程序,其實(shí)它的語義恰如狀態(tài)的替換。

OCL語言使用了大量的關(guān)鍵字(如self,context,pre,post等),其風(fēng)格類似于編程語言。

2.4 表達(dá)能力

從表達(dá)能力來分析,B語言的表達(dá)能力比OCL語言更強(qiáng),OCL語言只能對(duì)模型的約束加以說明,使用B方法編寫的規(guī)格說明具有精確性、無二義性、一致性、能進(jìn)行推理等特點(diǎn)。

OCL語言是一種半形式化的語言,正式的OCL1.5版本的規(guī)格說明中盡管對(duì)OCL語言的語法進(jìn)行了詳細(xì)的描述,但是沒有對(duì)其形式語義進(jìn)行過定義,而最新的OCL2.0版本的草案中提出了兩種語義,一種是基于元模型的語義,另一種是稱之為對(duì)象模型的集合論的形式語義已有研究人員指出這兩種語 義 存在著不一致性和不完備性。

2.5 前置條件、后置條件明確性

一個(gè)操作的前置條件是指在操作被執(zhí)行前必須為真的約束,一個(gè)操作的后置條件是指在操作執(zhí)行完成后必須為真的約束。在B語言中,前置條件是明確陳述的,冗余的前置條件需要一致性檢測(cè),OCL的前置條件也是明確給出的,用關(guān)鍵字Pre表示。在B中,不變式是冗余的,不變式的存在與否都不會(huì)改變操作的定義,它并不是操作后置條件的一部分,因而需要證明該操作是否必須保留不變式,而在OCL中,后置條件也明確給出了,用關(guān)鍵字Post表示。

2.6 工具支持

一種規(guī)格說明語言要得到廣泛的應(yīng)用,強(qiáng)有力的工具支持是至關(guān)重要的。一般而言,規(guī)格說明語言的支持工具可以分為下面幾種類型:

1)可視化編輯工具:主要是用于對(duì)規(guī)格說明語言進(jìn)行輸入和編輯。

2)語法檢查工具:是規(guī)格說明語言最基本的支持工具,其功能是用于檢查規(guī)格說明的語法正確性,但這種工具只能發(fā)現(xiàn)一些簡(jiǎn)單的語法錯(cuò)誤。

3)類型檢查工具規(guī)格說明語言均為類型語言使用類型檢查工具的目的是為了保證規(guī)格說明類型的正確性。

4)語義分析工具:是用來檢查規(guī)格說明的語義的正確性。

5)規(guī)格說明的求精:求精是指將規(guī)格說明轉(zhuǎn)換到程序代碼。

6)測(cè)試自動(dòng)化工具:測(cè)試自動(dòng)化是指從規(guī)格說明中產(chǎn)生測(cè)試用例,運(yùn)行測(cè)試用例和進(jìn)行測(cè)試結(jié)果分析的自動(dòng)化,這些工具能提高軟件開發(fā)的效率并且降低軟件維護(hù)費(fèi)用。

7)驗(yàn)證和確認(rèn)工具:主要是用于對(duì)規(guī)格說明進(jìn)行驗(yàn)證和確認(rèn),以保證規(guī)格說明具有所需要的性質(zhì)。驗(yàn)證和確認(rèn)方式主要有模型檢查,定理證明和動(dòng)畫技術(shù)三種。

OCL語言是一種相對(duì)較新的語言,因此目前該語言還沒有足夠的支持工具。大多數(shù)商業(yè)化的UML建模工具并沒有普遍提供對(duì)OCL語言的支持,只有一些研究人員對(duì)OCL的語義和支持工具進(jìn)行過研究。其相應(yīng)工作介紹如下:

1)OCL編輯工具目前主流的UML編輯工具如ArgoUML和MagicDraw等都提供了對(duì)OCL語言的支持,并提供了XMI格式的輸出。

2)詞法分析和類型檢查工具 首先出現(xiàn)的OCL支持工具是IBM公司出品的OCL詞法分析器,它是用Java和JavaCC詞法產(chǎn)生器編寫的。該分析器的功能包括語法分析和部分的類型檢查。后來出現(xiàn)的OCL詞法分析器偶Klasse Objecten公司出品的OCL詞法分析器,但它只能提供詞法分析。ArgoUML工具中集成了Dresden提供的OCL編譯器,它能提供完整的OCL語法和類型檢查。在MagicDraw工具中也可以對(duì)OCL語法進(jìn)行檢查。

3)其他OCL語言支持工具Bremen大學(xué)開發(fā)了USE(UML-based Specification Environment)系統(tǒng)工具。USE是一種用于信息系統(tǒng)規(guī)格說明的驗(yàn)證確認(rèn)工具。USE能對(duì)系統(tǒng)的模型進(jìn)行動(dòng)畫并規(guī)格說明和用OCL語言表達(dá)的非形式需求進(jìn)行確認(rèn),在對(duì)系統(tǒng)模型進(jìn)行動(dòng)畫的過程中用戶可以創(chuàng)建并操縱系統(tǒng)狀態(tài)。

B因?yàn)橛泄ぞ咧С侄@得相當(dāng)大的優(yōu)勢(shì),像B-Toolkit這種高質(zhì)量的商業(yè)軟件有一套完整的開發(fā)過程的支持用來完成如下一些任務(wù):類型檢測(cè)、動(dòng)畫、證明法則生成、交互或自動(dòng)的證明支持、代碼翻譯、文檔以及帶有配置管理功能的綜合開發(fā)環(huán)境支持。

2.7 生命周期的覆蓋

B支持從規(guī)格說明描述到詳細(xì)設(shè)計(jì)的軟件開發(fā)全過程,而OCL語言只能對(duì)系統(tǒng)模型的約束進(jìn)行說明,不能支持從規(guī)格說明的描述到詳細(xì)設(shè)計(jì)的軟件開發(fā)全過程。

3 實(shí)例分析

為了更好地展示兩種語言的特性,舉一個(gè)班級(jí)人數(shù)的實(shí)例,例如對(duì)于一個(gè)班級(jí)而言,只有注冊(cè)人數(shù)大于25人方可開課,并且由于教室大小的約束,人數(shù)又不能超過80人。我們來分別討論兩種形式化語言的規(guī)格說明:

3.1OCL規(guī)格說明

首先考慮如何對(duì)類的不變式進(jìn)行說明使用可以對(duì)班級(jí)人數(shù)的屬性加上如下的約束:

班級(jí)的學(xué)生人數(shù)必須大于25人并且小于80人。

Context Class

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

每個(gè)學(xué)生必須經(jīng)注冊(cè)后方能聽課

Context Student

Inv:self.isRegistered=true

對(duì)于操作而言,可以通過前置條件與后置條件加以輔助說明

Context Class::register(p:student)

Pre registerPre:class->excludes(p)

Post registerPost:class->includes(p)

上述的規(guī)格說明表示當(dāng)學(xué)生完成注冊(cè)以后學(xué)生成為班級(jí)的成員。

3.2 B規(guī)格說明

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 結(jié)束語

通過對(duì)B語言和OCL語言的比較,可以知道不同形式規(guī)格說明語言有各自的特點(diǎn)及適用范圍。OCL語言是一種文本性規(guī)格說明語言,但是沒有傳統(tǒng)形式語言的復(fù)雜性。作為UML標(biāo)準(zhǔn)的一部分,OCL被建模者用來說明UML的約束,如不變式、操作的前置、后置條件、狀態(tài)門限和屬性派生規(guī)則等,這大大增加了UML模型描述的精確性。然而,要使OCL表達(dá)式的解釋沒有二義性,必須給出OCL表達(dá)式語義的精確定義。OCL表達(dá)式語義描述有兩種可替換定義方法,使用UML元模型的標(biāo)準(zhǔn)描述形式和使用形式化的非標(biāo)準(zhǔn)描述形。B方法中的精化和實(shí)現(xiàn)是很多形式化開發(fā)方法所沒有的,它在規(guī)格說明的基礎(chǔ)上可直接生成可執(zhí)行系統(tǒng),并在整個(gè)開發(fā)過程中通過正確性驗(yàn)證,保證了軟件產(chǎn)品的高可靠性、可移植性和可維護(hù)性,從而可有效提高軟件的生產(chǎn)率。

參考文獻(xiàn):

[1] 鄒盛榮,鄭國(guó)梁. B語言和方法與Z、VDM的比較[J].計(jì)算機(jī)科學(xué),2002(10).

[2] 肖健宇,張德運(yùn). OCL數(shù)據(jù)類型到B形式化規(guī)約的轉(zhuǎn)換[J]. 計(jì)算機(jī)工程,2006(3):61-62.

[3] 陳怡海,繆淮扣. OCL與Object-Z作為UML約束語言的分析比較[J]. 計(jì)算機(jī)科學(xué),2004,31(12):182-183.