形式化語言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.