形式化描述語言Ｂ的面向對象機制研究

摘要：在分析B語言和面向對象方法的基礎上，提出一種具有面向對象特性的形式化描述語言B+，該語言克服原有B語言沒有機制形式描述一系列實例變量和不確定的行為的缺點。

關鍵詞：形式化；面向對象；B語言；B+

中圖分類號：TP301文獻標識碼：A文章編號：1009-3044(2008)20-30267-02

An Object-oriented System Research Based on Language B

DING Xiang-ling

(Huaihua College，Huaihua 418008，China)

Abstract:After analysing B language and object oriented method，the paper presents an object-oriented formal specification language named B+，which is an extension of B also.B+ overcomes the shortage of B language which doesn’t have mechanism to describe a series of example variable and uncertain behavior.

Key words:Formalism;Object-oriented;B language;B+

形式化方法、面向對象方法各有優缺點，兩者的結合能取長補短，促進面向對象軟件開發的自動化及形式化方法的實用化。在此我們對B語言進行了必要的擴充，使之成為一種面向對象的形式化規約語言B+，并將其作為目標語言

應用軟件形式規約的自動轉換中。

1 B語言與面向對象

B語言[1-2]是一種用于描述、設計計算機軟件的嚴格語言，其作用一直延伸到代碼生成，同時已經實現了一些工具系統，支持基于B語言的軟件開發的全過程。最早由法國人J.R.Abrail于20世紀80年代前期開始研究，目的是希望為實際軟件開發過程提供一個堅實的數學基礎。在B語言思想形成過程中，C.A.R.Hoare和E.W.Dijkstra的關于程序作為一個數學對象、前-后置謂詞、不確定性、最弱前置謂詞的概念，無疑是它的中心思想；同時，C.C.Morgan的重要思想“Programming from Specification”對其的形成起了深遠影響和巨大作用。使得該語言成為目前國際上最受重視的軟件形式化方法之一。

它處理的是軟件生存周期的核心方面，即技術性的規范化，產生層次性體系結構。其核心的抽象機操作[3]選擇廣義代換法能夠簡化證明需求，提供從抽象規格說明到過程代碼前后一致的符號表示法。一個廣義代換是一個抽象數學的編程結構，借助下列操作符，由基本代換x:=e建立起來的，它表示對狀態變量的賦值：

(1)S1[]S2：CHOICE S 1 OR S2 END

(2)P∣S ：PRE P THEN S END

(3)P==＞ S ：SELECT P THEN S END

(4)＠v.(P==＞S)：ANY v WHERE P THEN S END

(5)＠v.S：VAR v IN S END

面向對象方法最基本的特點是具有通過抽象數據類型實現對象類的建模[4-5]。雖然B語言具備封裝機制允許變量依附在操作中和通過機器重命名實現機器的各種實例。然而，在行為定義上，沒有機制使用上述語言形式描述一系列實例變量和不確定的行為。這種限制通過在B語言中，明確的建模一系列實例和以一系列實例為定義域的函數，對每個特征類建模加以克服。下面在保留B語言原有的基本數據類型、集合數據類型、笛卡爾積數據類型、AMN的基礎上詳細說明該機制的整個過程。

2 形式化描述語言B+

在B+中，貫穿與整個模型的約束和行為必須被轉換以反映狀態建模特征的轉換，從面向對象結構到B中基本結構變量的集合。我們把這種轉換記為T，則T(U)表示B+表達式U轉換為B。

如果一個B+表達式包含一個引用類特征a，屬于一個特定的實例x，在B+中寫作x.a.正如前面章節所描述，實例和他們特征值之間的關系以函數形式表示在B模型中。因此x.a轉換為函數應用a(x)。如果a是一個具有在目的端大于1的多重性關聯，則x與值集關聯。然而，由于關聯轉化為從客戶實例到供應端實例的子集的函數，對函數應用的轉換仍然有效。一個約束類的實例特征可能使用dot符號經過傳遞順序關聯連接被引用。例如，如果當前類的實例x，經過關聯a連接另一個類的實例，同時那個類有一個特征b，則對于關聯x的實例而言，值b在B+中作為x.a.b被引用。這就經過函數應用轉換了兩次，第一次是特征b，接著是特征a。因此，x.a.b經過b(x.a)到b(a(x))的轉換。然而，必須注意到如果a返回一個單獨實例，即如果關聯a有一個小于或等于1的多重性，這剛好有效。當多重性允許0個目標實例時，確保x在關聯中有個連接（即x:dom(a)）是非常重要的，否則a(x)是未定義的。

在B+中，（按照通常的面向對象風格），實例標識符（上面例子中的x）可能從一個對類特征值的引用中被忽略。引用有兩種不同含義，依賴與在何處發生。當引用在類操作之中，它表示的值屬于實例，因為該操作已經被調用(self)。在B模型中，一個參數this，其類型被作為操作參數添加，同時引用被轉換成a(this)。當引用沒有關聯一個操作，例如在invariant中依附與類，引用被明顯的產生在類所有實例中。在這個例子中，同樣的轉換，a(this)的引用a被使用并且完全的表達式封裝在全稱量詞中。例如，如果B+表達式U包含對類C特征的如此引用，表示為：?坌thisC · (thisC ∈ C?圯T(u))。

在B+中，操作符號可能包含類型化的且在B中將轉換為等效形式的參數表。在B機器代表的類中，輸入到操作返回類型域的字符將被使用作為操作返回標識。以同樣的方式，屬性，關聯，類操作（除了<>或<>）使用屬于類一個特點實例的數據立刻執行。因此操作需要知道類的哪個實例將執行。由于B不是面向對象的，通過增加參數thisCLASS，類型CLASS（CLASS是類名）到每個操作，操作必須明顯的關聯到類的一個特定實例。這可以通過在對屬性或類關聯的每個引用中作為實例參數使用。實例參數優于屬于操作的任何顯式參數被插入。操作行為的細節文本化詳細描述在操作B+說明的中守衛和行為中。因此，一個操作o，具有參數，p1，p2，……pn類型為T1，T2，……Tn，返回變量r1，r2，……rn將導致如下的形式化B操作：

r1，r2，..，rn← o(thisCLASS，p1， p2，...，pn) =

PRE thisCLASS ∈ CLASS ∧p1 ∈ T1∧p2 ∈ T2∧...∧pn ∈ Tn THEN

SELECT <> THEN <> END

END

守衛是B+謂詞包含包中任何的變量。行為是B+的替換，它經過描述在表1中的替換實現更新類的變量（屬性，關聯等）的值。

圖1中，PHONE有操作startCall，它試圖在channel tt上開始一個call，同時返回一個boolean表示它成功。如果channel當前沒有正在使用，call是成功的。

圖1 B+操作描述實例

操作startCall有個守衛tt∈channels，確保參數tt是一個關聯phone的channel。它的行為測試channel的屬性inUse:

IFtt.inUse = FALSETHENtt.inUse := TRUE || success := TRUE

ELSE success := FALSE END

操作在UML-B中完整的寫法:

Success← startCall (thisPHONE，tt) =

PRE thisPHONE ∈ PHONE∧ tt ∈ CHANNEL THEN

SELECT tt∈ channels(thisPHONE) THEN

IF inUse(tt) = FALSE THEN inUse(tt) := TRUE || success := TRUE

ELSE success := FALSE END

END

END

3 結束語

本文在分析B語言和面向對象方法的基礎上，提出一種具有面向對象特性的形式化描述語言B+，該語言克服原有B語言沒有機制形式描述一系列實例變量和不確定的行為的缺點。

參考文獻：

[1] Lano K，Haughton H.Formal Development in B Abstract Machine Notation[J].Information and Software Technoloy，1995，37(5-6):303-316.

[2] Wordsworth J B.Getting the Best From Formal Methods[J].Information and Software Technology，1999，41(4):1027-1032.

[3] J-R Abrial.B方法[M].裘宗燕，譯.電子工業出版社，2004.

[4] Goldsack S J， Kent S J H.Formal Methods and Object Technology:Formal Approaches to Computing and Information Technology[M].Springer-Verlag London Limited，1996.

[5] 徐家福，王志堅，翟成祥.對象式程序設計語言[M].南京:南京大學出版社，1992.

注：“本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。”