基于B方法的體系結(jié)構(gòu)描述語言的精化研究

丁湘陵

(懷化學(xué)院物理與信息工程系,湖南懷化 418008)

1 B方法和ABC/ADL體系結(jié)構(gòu)描述語言

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

ABC/ADL體系結(jié)構(gòu)描述語言[3-6]是北京大學(xué)信息科學(xué)技術(shù)學(xué)院梅宏等人設(shè)計的一種通用軟件體系結(jié)構(gòu)描述語言,以面向?qū)ο蠓治龊驮O(shè)計方法為主導(dǎo),主要概念包括構(gòu)件、連接子和體系機構(gòu)風(fēng)格,并吸取了面向Aspect的開發(fā)思想,最突出的特點是支持軟件體系結(jié)構(gòu)描述向詳細設(shè)計和實現(xiàn)的映射,并支持構(gòu)件的組裝,使用復(fù)合構(gòu)件和復(fù)雜連接子逐步精化系統(tǒng),但缺乏語義支持.

于是,將B方法和ABC/ADL兩相結(jié)合,取長補短,展開了體系結(jié)構(gòu)精化的研究,提出了一種使兩者無縫集成的精化開發(fā)方法：首先定義精化約束和規(guī)則保證在精化過程中模型系統(tǒng)的一致性;然后對ABC/ADL復(fù)合構(gòu)件和復(fù)雜連接子使用定義的精化約束和規(guī)則逐步精化,直到可執(zhí)行程序.

2 體系結(jié)構(gòu)精化研究

2.1 復(fù)合構(gòu)件和復(fù)雜連接子[5]

ABC/ADL提供復(fù)合構(gòu)件和復(fù)雜連接子的機制來幫助設(shè)計人員逐步精化系統(tǒng).從構(gòu)件對外的角度來看,復(fù)合構(gòu)件和原子構(gòu)件沒有區(qū)別,因此它需要所有原子構(gòu)件規(guī)約中的部分：模板規(guī)約、屬性規(guī)約、Player規(guī)約等.不同點在于復(fù)合構(gòu)件還需要定義內(nèi)部結(jié)構(gòu)規(guī)約,內(nèi)部結(jié)構(gòu)規(guī)約定義了內(nèi)部體系結(jié)構(gòu)名,它指向一個體系結(jié)構(gòu)定義;還定義了若干個映射規(guī)約,每個規(guī)約將復(fù)合構(gòu)件自身的一個Player映射到內(nèi)部體系結(jié)構(gòu)某個構(gòu)件的Player.圖1是例子中復(fù)合構(gòu)件Ticket Agent的定義,它的內(nèi)部結(jié)構(gòu)是一個名為TA的體系結(jié)構(gòu),seller是在TA中定義的一個構(gòu)件實例,復(fù)合構(gòu)件的Player get Order Sheet被映射為seller的Player get Order Sheet.

圖1 復(fù)合構(gòu)件定義

從與構(gòu)件連接的角度看,復(fù)雜連接子和簡單連接子沒有區(qū)別.類似復(fù)合構(gòu)件,它有自己的內(nèi)部結(jié)構(gòu);但是與復(fù)合構(gòu)件不同的是,復(fù)雜連接子的角色要被映射為內(nèi)部結(jié)構(gòu)中某個連接子實例的角色.

2.2 構(gòu)件或者連接子精化理論

在ABC/ADL中使用復(fù)合構(gòu)件和復(fù)雜連接子逐步精化系統(tǒng),但缺乏理論基礎(chǔ).本節(jié)將介紹使用經(jīng)過事件機制擴展的B方法來證明精化的合理性和保證構(gòu)件和連接子精化過程的無死鎖性,并在此基礎(chǔ)上精化到可執(zhí)行代碼.這里以構(gòu)件模型來加以說明,連接子模型可以類推.在詳細介紹精化過程之前,先引入2個約束和3個規(guī)則并加以適當闡述.

在精化過程中可能包含更多的變量和更多的事件,而這些事件必須滿足下面提出的約束1和約束2才能被引入,這樣才能保證在精化過程中模型系統(tǒng)的一致性.

約束1：事件的守衛(wèi)精化必須是正確的 (在當前的不變量內(nèi)),這是因為決不讓構(gòu)件進入死鎖狀態(tài).(注意：在構(gòu)件的初始情況下顯然是不存在死鎖狀態(tài)的).

約束2：在精化過程中引入的新的事件不允許永遠執(zhí)行,這意味著這些事件必須一直減少一個確定的自然數(shù)變量或者一個確定的有限集合.

將最終的事件轉(zhuǎn)化為可執(zhí)行代碼必須遵循一定的轉(zhuǎn)化規(guī)則,在這里提出三條規(guī)則,規(guī)則1將事件提出來,規(guī)則2和規(guī)則3將事件合成一個結(jié)果代碼.在提出規(guī)則之前,首先說明一些符號的含義,S為事件 (被守衛(wèi)著的執(zhí)行)的選擇;?為守衛(wèi)操作;讓 []為選擇操作.

規(guī)則1：

S→S’[]U

Condition

S?S’ skip?U I?grd(S’) ∨grd(U) I?V∈N

I? (V=n? [U](V

規(guī)則1中?說明數(shù)據(jù)精化操作,新的事件U精化skip并將自然數(shù)變量減少,這些條件本質(zhì)上驗證了規(guī)則1在約束1和約束2中是滿足的.

規(guī)則2：

(P∧Q) ?S[](P∧┐Q?T)[]U→ (P?IF Q Then S else T)[]U

規(guī)則2的作用是在風(fēng)格上使兩個事件合為一體形成一個IF語句.

規(guī)則3：

(P∧Q) ?S[](P∧┐Q?T)[]U→ (P?While Q Do S End;T)[]U

Condition：S和T沒有被守衛(wèi)

∧P∧Q?[S]P

注意：在守衛(wèi)Q下循環(huán)體S應(yīng)該維持P不變式.規(guī)則3有兩種特殊情況：①當謂詞P簡單消失 (在這種情況中通過條件的第二條來嚴格限制),②當T精化為skip.

在前面已經(jīng)知道如何通過規(guī)則1將一個新的事件引入進來,該事件必須精化skip并且同時減少一個確定的自然數(shù)或者一個有限的集合,同樣該變量在相應(yīng)的精化步驟中也可能引入一些新的變量.

為了容易實現(xiàn)這個規(guī)則,就必須進行如下操作：假設(shè)一個變量y被正常引入,具有類型Sy,并且具有一些粘結(jié)不變量.在精化Ri+1步,同樣假設(shè)一個新的事件NewEvent在該事件引入.假設(shè)一個相應(yīng)的變量由NewEvent去減少,表示為一個自然數(shù)表達式V(y).設(shè)想由被引入的變量y和前一階段Ri的事件NewEvent組成加上維持變量y在其類型允許范圍內(nèi)的最小可能并減少V(y)的量.粘結(jié)不變式?jīng)]有被引入Ri,仍在Ri+1中,這樣就會以如下形式執(zhí)行：NewEventBegin y：y∈Sy∧V(y)

約束和規(guī)則提出之后,下面以構(gòu)件的精化過程為例加以說明：構(gòu)件首先被刻畫為一些參數(shù),這些參數(shù)暗示將來程序的一些不變的輸入,也就是說在將來它們運行時,它們將不改變這些參數(shù),如Parameters∈Sp,Sp說明了參數(shù)類型.同樣它也具有一些變量,稱之為結(jié)果 (results).這些變量被定義為Sr類型,如：results∈Sr.由參數(shù)和變量可以得到該構(gòu)件的初始規(guī)約描述,獲得抽象的player和computation.構(gòu)件的精化主要針對computation處理,computation可以通過約束1和約束2精化為更小的內(nèi)部實體computationi,針對每個小實體同樣可以使用約束1和約束2進行進一步精化轉(zhuǎn)化為事件.不過也要注意一點：可能沒有computationi而直接精化到具體的事件.事件已經(jīng)是可精化的最小單元.通過研究觀察,可能發(fā)現(xiàn)這些事件具有輸入或者輸出的功能,如果它們與player具有相同的功能或者行為,可以將它們與player進行mapping,這樣就得到了復(fù)合構(gòu)件.如果沒有任何關(guān)聯(lián),事件就轉(zhuǎn)化為構(gòu)件的method.最后,只需要使用規(guī)則1、2、3就可以將所有事件進行綜合得到構(gòu)件的最終可執(zhí)行代碼.

3 實例研究

本節(jié)介紹一個簡單數(shù)據(jù)庫系統(tǒng)的完整開發(fā)過程,使用上節(jié)介紹的方法,將初始的構(gòu)件模型和連接子模型精化為具有眾多事件的事件系統(tǒng),分析事件和player或role的關(guān)系得到復(fù)合構(gòu)件或復(fù)雜連接子并最終精化到可執(zhí)行代碼.

在這個例子里,要描述的是保存某個人群中個人信息的系統(tǒng).假定出現(xiàn)在數(shù)據(jù)庫里的個人都有一個性別 (male或female)和一個狀態(tài) (living或dead),因此,需要定義兩個枚舉集合SEX和STATUS,還要定義一個集合PERSON,定義如下：SEX{male,female};STATUS={living,dead}.這些集合除了具有數(shù)據(jù)之外還有對相應(yīng)數(shù)據(jù)的各種操作.例如：r←SEX-READBegin r：∈SEX End;SEX-WRITE(i)=PRE i∈SEX Then skip End.這里就是對集合SEX的操作,對于其他集合也具有類似的操作,在此不詳細描述.

首先分析該系統(tǒng)應(yīng)實現(xiàn)的功能：對于輸入的個人信息執(zhí)行相應(yīng)的操作,比如說當前一位嬰兒誕生,就必須對他進行登記,將他的相關(guān)信息輸入并調(diào)用相關(guān)的操作 (birth-operation)對數(shù)據(jù)庫文件進行修改.由此,該系統(tǒng)必須具有的變量：person,sex,status,mother,husband,wife,command.它們對應(yīng)的不變式如下：person?PERSON∧sex∈person→SEX∧status∈person→STATUS∧mother∈person→ (MARRIED∩WOMAN) ∧husband∈WOMAN →MAN∧wife=husband-1∧command∈COMMAND其中MAN=sex-1[{man}];WOMAN=sex-1[{woman}];LIVING=status-1[{living}];DEAD=status-1[{dead}];MARRIED=Dom(husband∪wife);SING LE=person-MARRIED;ANG LE=PERSON-person;COMMAND = {new,birth,marriage,death,print,quit}.現(xiàn)在研究該系統(tǒng)所具有的事件,對于輸入的控制命令command做出相應(yīng)的操作來獲得所必需的person,sex,稱之為incom事件;事件trandata接受由in-com事件傳遞過來的數(shù)據(jù),同時將數(shù)據(jù)傳遞給下一事件;最后一個事件接收傳送來的數(shù)據(jù),進行簡單的數(shù)據(jù)檢驗,在這里要提供一個變量b來標明數(shù)據(jù)是否合格,如果b為true,則進行與command對應(yīng)的操作內(nèi)容;如果為false,則輸出錯誤原因或錯誤信息,這個事件稱之為operation-data.該系統(tǒng)的數(shù)據(jù)傳遞過程如圖2所示,顯然這是一個典型客戶/服務(wù)器風(fēng)格的系統(tǒng).

圖2 數(shù)據(jù)傳遞圖

基于上面分析,初始模型分解如表1所示.

表1 初始模型分解表

觀察表1發(fā)現(xiàn)person,sex在三個模型中都存在,但是可能希望在事件的演變過程中對person,sex進行精化,這就意味著它們不能成為共享變量,必須把它們從相對獨立的模型中分離出來并且提出中間變量作為模型之間交流的數(shù)據(jù).由于Server的數(shù)據(jù)也是由Client端發(fā)送過來的,所以在這里引入中間變量p1,s1與Client的person,sex相關(guān)聯(lián).另兩個中間變量p2,s2和Client的p1,p2相關(guān)聯(lián),這樣就將Client和Server中的person和sex就被間接消除掉了.數(shù)據(jù)的精化結(jié)果如表2所示.

表2 數(shù)據(jù)精化結(jié)果表

對于Server模型 (即Server構(gòu)件)具有兩個輸入數(shù)據(jù)p2和s2以及輸出操作成功與否.其初始構(gòu)件規(guī)約描述為：

初始事件receive可以描述為：receive(p2,s2)p2∈PERSON∧s2∈SEX End.現(xiàn)研究一下Server構(gòu)件的內(nèi)部規(guī)約computation.對于不同的COMMAND控制命令,數(shù)據(jù)庫中數(shù)據(jù)的修改也將產(chǎn)生不同的事件,事件的發(fā)生是非常不確定的,new?first-human(s);birth?new-born(s,w);marriage?marriage(w,m);death?death(p);print?printperson(p);同時這些事件在任意時刻只有一個可以發(fā)生.這里只對在command=new的情況進行分析,其他情況可以相似類推.command=new對應(yīng)的數(shù)據(jù)庫操作first-human(s)初始化描述為：first-human(s)∈SEX End.進一步精化描述為：

對于該事件可以更進一步的精化斯之產(chǎn)生可執(zhí)行代碼,首先將上面相應(yīng)的數(shù)學(xué)符號具體化.于是引入事件：baby←createobject;mod-field(1,baby,code-SEX(s));mod field (2,baby,code-STATUS(living)).

第一個事件實現(xiàn)產(chǎn)生集合對象并返回一個該對象的實例,第二、三個事件設(shè)定實例的性別和狀態(tài).對于第一個事件更進一步分析發(fā)現(xiàn)對于一個新生的嬰兒必然在數(shù)據(jù)的文件中產(chǎn)生記錄,由此提出文件變量,它包含最多maxrec的記錄值的有窮序列和一個具體的變量bufvrb,定義如下：file∈seq(FIELD→VALUE) ∧size(file) ≤max-rec∧buf-vrb∈INDEX→VALUE.

相應(yīng)操作如下：

基于文件變量,可以將第一個事件精化為如下形式：baby←create object=Begin NEWRECORD(v);baby←SIZEFILE End;而對于第二和第三個事件發(fā)現(xiàn)它們具有共同點,對此提出一個通用事件modfile(o,i,v)PRE o∈Dom(file) ∧i∈FIELD∧v∈VALUE Thenfile(o)(i)：=v End.這樣得到了對于new操作的所有事件.使用同樣方法可以得到其他操作事件.但是在這里還必須提出關(guān)于數(shù)據(jù)狀態(tài)的檢測機制,因此,引入如下事件來檢測數(shù)據(jù)的正確性.

is-present(p);is living(p);is woman(p);is-married(p);has mather(p);valstatus(p);valsex(p);val spouse(p);valmother(p).到此,Server模型的所有事件就都已經(jīng)提出來了.

仔細分析,發(fā)現(xiàn)Server的扮演者receive與firstname、new-born、marriage、death、print-person具有相同的行為：都需要輸入數(shù)據(jù)p2或者s 2,由此可以將它們進行映射;扮演者send輸出操作結(jié)果與在各個操作中的STRING-WRITE具有同樣行為,可以將它們進行映射 (注意：代碼實現(xiàn)時要加以改進將各個操作中的STRING-WRITE提煉出來),這樣Server也具有了復(fù)合結(jié)構(gòu),在這里只描述了部分映射關(guān)系,其它也可類似得到.

到此為止,Server構(gòu)件完成了精化,但本文的目標并不僅僅到此,而是必須按照規(guī)則精化到可執(zhí)行代碼.由此將已經(jīng)提出的事件按照定義的約束和規(guī)則綜合,得到如下可執(zhí)行代碼.

觀察SERVER模型的實現(xiàn),發(fā)現(xiàn)還必須設(shè)計了一些關(guān)于文件的操作：

到此,一個簡單數(shù)據(jù)庫系統(tǒng)的設(shè)計已經(jīng)告一段落.現(xiàn)在必須完善的就是對于這種設(shè)計結(jié)果正確與否,還必須對事件進行證明.比如說,要驗證事件death(p)的正確性,就必須維持不變式,這點可以描述為如下形式：

通過執(zhí)行有關(guān)代換,除去不需要的假設(shè)及其明顯的結(jié)論,將只需要證明公式：

STATUS={living,dead}

status∈person→STATUS

p∈PERSON

?[status：=status<+ {p→dead}]∈person→STATUS.使用工具Prob很容易將其實現(xiàn).具體的使用在這里不詳細介紹.對于連接子Clink和Client構(gòu)件可以按照Server構(gòu)件描述的方法實現(xiàn).

4 結(jié)束語

本文展開了體系結(jié)構(gòu)精化的研究,提出了一種使兩者無縫集成的精化開發(fā)方法：首先定義精化約束和規(guī)則保證在精化過程中模型系統(tǒng)的一致性;然后對ABC/ADL復(fù)合構(gòu)件和復(fù)雜連接子使用定義的精化約束和規(guī)則逐步精化,直到可執(zhí)行程序.同時將該方法應(yīng)用到人口統(tǒng)計的數(shù)據(jù)庫系統(tǒng),應(yīng)用工具ProB驗證該系統(tǒng)的動態(tài)行為.但是,基于ABC/ADL描述框架中的求精過程是一個復(fù)雜而且困難的工作且基于不變式性質(zhì)不變的前提來實現(xiàn)求精過程,還需人工的操作,考慮開發(fā)可集成的驗證工具集成到ABC/ADL開發(fā)工具中達到抽象模型到具體代碼實現(xiàn)的求精過程的驗證自動化.總之,使基于ABC/ADL結(jié)構(gòu)框架的程序設(shè)計過程更加高效、可靠,且保證設(shè)計過程的正確性和可復(fù)用性是最終目的.

[1]J-R Abrial著.B方法 [M].裘宗燕譯.北京：電子工業(yè)出版社,2004.

[2]T.Lecomte.Event B Reference Manual IST-1999-11435[EB/OL].http：//www.atelierb.eu/ressources/evt2b/eventb-reference-manual.pdf.2010.

[3]Hong Mei,Jichuan Chang,Fuqing Yang,Composing S of tware Components at Architectural Level[C].//In Proceedings of International Conference on S of tware-Theory and Practice,IFIP the 16th World Computer Congress(WCC2000/ICS2000),2000,(8)：224-231.

[4]Hong Mei,Feng Chen,Qianxiang Wang,and Yaodong Feng,ABC/ADL：An ADL Supporting ComponentComposition[C]//Proceedings of 4th International Conference on Formal Engineering Methods,ICFEM2002,Oct.2002：38-47.

[5]王曉光,馮耀東,梅 宏.ABC/ADL：一種基于XML的軟件體系結(jié)構(gòu)描述語言 [J].計算機研究與發(fā)展,2004.9,Vol.41,No.9：1521-1531.

[6]梅宏.基于體系結(jié)構(gòu)、面向構(gòu)件的軟件開發(fā)方法ABC[C].//中國科學(xué)院信息技術(shù)科學(xué)部第19次技術(shù)科學(xué)論壇“軟件技術(shù)”專題學(xué)術(shù)報告會,2006：1-8.