基于模型驅(qū)動(dòng)的Web應(yīng)用服務(wù)系統(tǒng)開(kāi)發(fā)理論框架

侯金奎，鹿旭東，陳春雷，王 磊

1(濰坊學(xué)院 計(jì)算機(jī)工程學(xué)院,山東 濰坊 261061)

2(山東大學(xué) 軟件學(xué)院，濟(jì)南 250061)

1 引 言

近年來(lái)，隨著云計(jì)算的服務(wù)模式在業(yè)界的廣發(fā)應(yīng)用和迅猛發(fā)展，基于網(wǎng)絡(luò)的服務(wù)系統(tǒng)正在不斷替代傳統(tǒng)意義上的計(jì)算系統(tǒng)和軟件系統(tǒng)[1].Web服務(wù)是落實(shí)云計(jì)算環(huán)境中各類資源及能力交付和使用模式的主要方式，可以方便地滿足用戶需求，是實(shí)現(xiàn)面向服務(wù)計(jì)算的主要技術(shù)[2].大型復(fù)雜Web系統(tǒng)在其模型描述和系統(tǒng)演化的過(guò)程中，需保持清晰、易理解、可追蹤、可驗(yàn)證、易修改[3].針對(duì)大型Web服務(wù)系統(tǒng)的建模、開(kāi)發(fā)以及系統(tǒng)重構(gòu)技術(shù)和方法進(jìn)行研究，為此類系統(tǒng)的設(shè)計(jì)和實(shí)現(xiàn)提供有效的方法學(xué)指導(dǎo)，提出有效的技術(shù)手段來(lái)提升軟件研發(fā)的質(zhì)量和效率，已成為當(dāng)前面向服務(wù)的軟件工程面臨的一個(gè)亟待解決的重要任務(wù)[4].已有的研究都是針對(duì)特定的應(yīng)用領(lǐng)域和場(chǎng)景[5,6]，提出的實(shí)現(xiàn)方案[7]，但這些工作并不能對(duì)一般意義下大型復(fù)雜Web系統(tǒng)的模型演化和特性考察提供支持.

采用模型驅(qū)動(dòng)的軟件開(kāi)發(fā)(model driven software development)方法是應(yīng)對(duì)軟件開(kāi)發(fā)和維護(hù)復(fù)雜性的一種有效手段，它以模型為核心制品，通過(guò)一系列的模型轉(zhuǎn)換來(lái)生成最終的目標(biāo)系統(tǒng)[8].模型驅(qū)動(dòng)開(kāi)發(fā)作為一種開(kāi)放性的理念和模式，已經(jīng)被學(xué)術(shù)界和業(yè)界廣泛接受并表現(xiàn)出了極強(qiáng)的生命力[6,7].模型轉(zhuǎn)換是模型驅(qū)動(dòng)軟件開(kāi)發(fā)的關(guān)鍵步驟，以實(shí)現(xiàn)不同抽象層次模型之間的轉(zhuǎn)換和精化[9].為了支持模型驅(qū)動(dòng)開(kāi)發(fā)中的模型的自動(dòng)轉(zhuǎn)換，需要精確地定義和描述模型以及模型的變化.從技術(shù)發(fā)展的角度看，基于構(gòu)件和構(gòu)件組裝的工業(yè)化軟件開(kāi)發(fā)仍是快速構(gòu)造系統(tǒng)、降低開(kāi)發(fā)費(fèi)用、減輕維護(hù)負(fù)擔(dān)的主流方案[10].市場(chǎng)和業(yè)界多年來(lái)的實(shí)踐和驗(yàn)證也都表明，基于構(gòu)件的軟件工程和模型驅(qū)動(dòng)開(kāi)發(fā)方法的結(jié)合是成功的，發(fā)展前景良好.

范疇理論[11]描述能力強(qiáng)，可為Web服務(wù)系統(tǒng)的層次結(jié)構(gòu)提供形式化的語(yǔ)義描述.在我們的前期工作中[12-14]，已將范疇理論用于軟構(gòu)件和體系結(jié)構(gòu)模型之間映射關(guān)系的描述.本文進(jìn)一步擴(kuò)展了這種思想，從軟件設(shè)計(jì)實(shí)踐和基于體系結(jié)構(gòu)，面向軟構(gòu)件和設(shè)計(jì)模式的軟件設(shè)計(jì)出發(fā)，提出了軟件設(shè)計(jì)和精化中的模型轉(zhuǎn)換和模型驅(qū)動(dòng)的軟件開(kāi)發(fā)理論框架.設(shè)計(jì)模式看成是構(gòu)件規(guī)范的模版，模板的實(shí)例化和規(guī)范的集成過(guò)程就是軟件設(shè)計(jì)和實(shí)現(xiàn)的過(guò)程，在此基礎(chǔ)上，建立起了模型轉(zhuǎn)換和精化中特性描述和一致性研究的統(tǒng)一框架.應(yīng)用研究表明，該框架符合模型驅(qū)動(dòng)軟件設(shè)計(jì)的本質(zhì)要求，為模型轉(zhuǎn)換和模型驅(qū)動(dòng)的Web應(yīng)用服務(wù)開(kāi)發(fā)提供了新的認(rèn)知、分析和研究的指導(dǎo)架構(gòu).

2 模型定義

參考文獻(xiàn)[13]、[14]和[15]，本文給出標(biāo)識(shí)、對(duì)象類型、對(duì)象關(guān)系等定義.在此基礎(chǔ)上，進(jìn)一步定義規(guī)范、規(guī)范轉(zhuǎn)換、規(guī)范模板及規(guī)范集成等概念.

定義1.構(gòu)件對(duì)象標(biāo)識(shí)(Component Object Signature). 標(biāo)識(shí)Scmp=是一個(gè)三元組.其中,SDT是一個(gè)數(shù)據(jù)類型標(biāo)識(shí)，SAT是構(gòu)件的特性符號(hào)組成的集合，SAC是構(gòu)件的動(dòng)作符號(hào)組成的集合.

定義2.構(gòu)件對(duì)象類型(Component Object Type).對(duì)象類型是構(gòu)造具有序偶OTcmp=所描述共同特性的對(duì)象實(shí)例的模版,其中Scmp是一個(gè)構(gòu)件對(duì)象的標(biāo)識(shí)，SAX是一個(gè)Scmp相關(guān)公式和公理組成的集合.

定義3.對(duì)象關(guān)系類型(Types of Object Relationships). 定義對(duì)象關(guān)系機(jī)制集合為R={R1，…，Rm>0}.其中每一個(gè)Ri是具有特定機(jī)制的對(duì)象間關(guān)聯(lián)方式.對(duì)于給定的對(duì)象類型集合OT={OT1,…，OTn>0}.對(duì)象關(guān)系類型集合RT=={RT1，…，RTu>1}.其中每一個(gè)RTi=Ri,是一個(gè)具有類型Ri∈R的對(duì)象類型OTp∈OT和OTq∈OT間有向序偶關(guān)系.

對(duì)象關(guān)系機(jī)制是由軟件的模型或平臺(tái)所提供和決定的[12].常見(jiàn)的關(guān)系機(jī)制有：方法調(diào)用、事件激發(fā)、消息發(fā)送、數(shù)據(jù)傳送、遠(yuǎn)程過(guò)程調(diào)用等.特定對(duì)象間的關(guān)系是受到對(duì)象類型和關(guān)系機(jī)制約束的.這是軟件構(gòu)造實(shí)踐中考察一個(gè)系統(tǒng)內(nèi)對(duì)象或構(gòu)件間關(guān)系兼容性的基本必要條件.

定義4.對(duì)象關(guān)系實(shí)例的標(biāo)識(shí).對(duì)于對(duì)象關(guān)系類型RTi=Ri，它的一個(gè)關(guān)系實(shí)例是RO=Ri，它是由ORType標(biāo)識(shí)以及由該標(biāo)識(shí)形成的對(duì)象類型所生成的實(shí)例(參見(jiàn)圖1)；其中，Xp∈X(OTp)，EqE(OTq).

該標(biāo)識(shí)名是用于表達(dá)和生成對(duì)象關(guān)系實(shí)例的.圖1給出了對(duì)象關(guān)系實(shí)例的標(biāo)識(shí)和對(duì)象類型的結(jié)構(gòu)框架.其中,GetActionNames獲得在SO的Gso動(dòng)作中調(diào)用DO.Gdo動(dòng)作的文字說(shuō)明，被用于改寫SO對(duì)象中Gso動(dòng)作的行為；Σ代表對(duì)字符串的并置運(yùn)算.

定義5.類型化范疇(Typed Category). 類型化范疇[16]是一個(gè)5元組TC=，其中：OT是非空對(duì)象類型集合，R是非空對(duì)象關(guān)系機(jī)制集合，RT是非空對(duì)象關(guān)

ORType//RTi=Ri的關(guān)系實(shí)例的標(biāo)識(shí)

//和對(duì)象類型Ri

圖1 對(duì)象關(guān)系類型的標(biāo)識(shí)和對(duì)象類型Fig.1 Signature and object type of types of object relationships

系類型集合，O={O1,…，On>0}(Oi的類型∈OT)是非空對(duì)象實(shí)例集合，F(xiàn)={F1，…，F(xiàn)m≥0}(Fi的類型Ri∈RT)是對(duì)象關(guān)系實(shí)例集合,其中Fi=Ri，Xp∈X(OTp)，EqE(OTq).由此，TC：(1)為f∈F指派一個(gè)操作,它是從f定義域的一個(gè)對(duì)象實(shí)例a∈O到f值域的一個(gè)對(duì)象實(shí)例b∈O,如果a= domf并且b= codf,那么f被表示為f:a→b；(2)為g，f∈F的關(guān)系對(duì)指派一個(gè)合成操作.,它是f與g的合成,記為g.f:domf→ codg,其中domg= codf.

由定義5，軟件體系結(jié)構(gòu)模型(Software Architecture)就是一個(gè)類型化范疇SA=.

根據(jù)類型化范疇的定義,極端情況下體系結(jié)構(gòu)只有一個(gè)構(gòu)件對(duì)象構(gòu)成.

定義6.體系結(jié)構(gòu)的標(biāo)識(shí)及其對(duì)象類型. 由SAType()構(gòu)造的標(biāo)識(shí)以及由該標(biāo)識(shí)形成的對(duì)象類型，是用于表達(dá)體系結(jié)構(gòu)語(yǔ)義和生成體系結(jié)構(gòu)實(shí)例的一個(gè)特別的標(biāo)識(shí)以及由該標(biāo)識(shí)形成的對(duì)象類型.

圖2給出了由體系結(jié)構(gòu)范疇構(gòu)造標(biāo)識(shí)和對(duì)象類型的結(jié)構(gòu)框架.其中，addTo()動(dòng)作用文字串s改寫對(duì)象so的動(dòng)作Gso的內(nèi)容，由此改寫了Gso的行為構(gòu)成.

注意，某些構(gòu)件類型是不能通過(guò)外部改寫其行為特性的.這時(shí)，應(yīng)該限制其只能接受操作，而不能向其他對(duì)象發(fā)出操作.

3 服務(wù)模型轉(zhuǎn)換

規(guī)范引入了范疇符號(hào)和操作符號(hào)，并且定義了實(shí)現(xiàn)或被規(guī)范的模型必須具有的特性[17].

定義7.構(gòu)件規(guī)范(Component Specification).規(guī)范SP是一個(gè)序偶，其中SA=是一個(gè)體系結(jié)構(gòu)，Φ是一個(gè)由SA成份構(gòu)成的SA-句子匯集.所有SA-句子的集合表示為Sen[SA].

SAType//體系結(jié)構(gòu)范疇的標(biāo)識(shí)和對(duì)象類型

圖2 體系結(jié)構(gòu)類型的標(biāo)識(shí)和對(duì)象類型Fig.2 Signature and object type of types of software architecture

規(guī)范SP=的模型是一個(gè)SA-模型M，其中對(duì)每一個(gè)ψ∈Φ有M┝ψ.所有這種模型M的集合表示為Mod[SP].

為簡(jiǎn)便，以后的討論中規(guī)范的特性集也用規(guī)范的名稱表示.

定義8.規(guī)范態(tài)射(Specification Morphism).從規(guī)范SP=到規(guī)范SP′ =的一個(gè)規(guī)范態(tài)射，是一個(gè)體系結(jié)構(gòu)態(tài)射σ:SA→SA′，使得每一個(gè)模型M∈Mod[SP′]可有M|σ∈Mod[SP]，其中M|σ是M的反函子(reduct functor).規(guī)范態(tài)射可表示為σ：SA→SA′.

函子(Functor)F(A，B)是從范疇A到范疇B的函數(shù)，它為每一個(gè)A對(duì)象指派一個(gè)B對(duì)象，并為每一個(gè)A中f：a→b指派一個(gè)B中F(f)：F(a)→F(b)，使得等態(tài)射和合成關(guān)系得到保持.Functor定義了范疇A到B的變換關(guān)系.反函子Reduct functor是與函子相反的變換.給定范疇A、B，從A到B的函子F定義了A是如何被包含在B中，而F的反函子B|F定義了B是如何從A形成的.

定義9.規(guī)范態(tài)射的類型(Types of Specification Morphism).設(shè)SP={S1，…，Sm>0}是所有規(guī)范的集合.規(guī)范態(tài)射是滿足特定約束C的兩個(gè)或多個(gè)規(guī)范之間的有向關(guān)系，具體形式有{S1，…，Sn>0} →t∈STS和S→t∈ST{S1，…，Sn>0}，其中S∈SP和Si∈SP都是規(guī)范，ST是有限規(guī)范態(tài)射的關(guān)系類型，ST={轉(zhuǎn)換/t，分解/a，選擇/o，And合成/ac，Or合成/oc，集成/i，復(fù)制/d，不計(jì)類型/st}.

轉(zhuǎn)換和復(fù)制都是與常規(guī)概念類似的簡(jiǎn)單的規(guī)范態(tài)射，其它則是與常規(guī)概念不同的復(fù)雜規(guī)范態(tài)射.

定義10.轉(zhuǎn)換(Transformation).轉(zhuǎn)換F具有形式F:S1→TS2，其中S1，S2∈SP都是規(guī)范，→T代表有向關(guān)系為轉(zhuǎn)換的規(guī)范態(tài)射關(guān)系，并滿足以下特性：每一個(gè)S1中的對(duì)象a映射為S2中的對(duì)象b;為每一個(gè)S1中的關(guān)系f：a→b映射為S2中的一個(gè)關(guān)系F(f)：F(a) →F(b);a∈S1有F(ida) =idF(a);并且，對(duì)于S1中的關(guān)系合成g°f,有F(g°f) =F(g)°F(f).

圖3(a)給出了轉(zhuǎn)換的圖式表達(dá)，圖3(c)給出了多次轉(zhuǎn)換關(guān)系的合成關(guān)系.轉(zhuǎn)換關(guān)系及其合成可以用來(lái)表達(dá)在語(yǔ)義保持的約束下從模型到實(shí)現(xiàn)的軟件精化過(guò)程.

定義11.規(guī)范模版(Template of Specification). 規(guī)范模版[14]是一個(gè)規(guī)范類型SP(T1s1:t1,…,Tnsn:tn>0)的，其中，Tksk∶tk表示用于SP實(shí)例化的參數(shù)，Tk是形式參數(shù)，si是其類型，ti表示參數(shù)的傳送方式，可以是替換或引用的方式來(lái)實(shí)現(xiàn)參數(shù)傳送.

簡(jiǎn)言之，規(guī)范模版是一個(gè)還沒(méi)有實(shí)例化的規(guī)范.如果不需要，可以不區(qū)分規(guī)范和規(guī)范模版，而通稱為規(guī)范.

定義12.規(guī)范模版的實(shí)例化(Instantiation of Specification Template).規(guī)范模版SP(T1s1∶t1，…，Tnsn∶tn>0)被規(guī)范S的實(shí)例化表示為運(yùn)算=S<+SP(t1，…，tn)，其中，tk是S或S中某成份的標(biāo)識(shí)，M是實(shí)例化后得到的規(guī)范實(shí)例，它是用S或S中的成份替換SP中相應(yīng)成份后得到的規(guī)范.S可以是一個(gè)規(guī)范集合，此時(shí)，tk∈S或tk是S中某規(guī)范的某成份標(biāo)識(shí).同理，可以定義實(shí)例化運(yùn)算=SP(t1，…，tn)+>S.

定義13.集成(Integration).規(guī)范S1，S2∈SP的集成是一個(gè)新的規(guī)范,記為S=S1+S2,+∈{<+,+,},表示按照特別的運(yùn)算關(guān)系計(jì)算得到規(guī)范S；其中，S=S1S2表示按特性合一運(yùn)算[14]；S=S1<+S2表示以S1為核通過(guò)結(jié)合S2獲得S；S=S1+>S2表示以S2為核通過(guò)結(jié)合S1獲得S.

定義14.集成的框與核(frame，kernel of Integration).當(dāng)規(guī)范S1，S2∈SP發(fā)生S=S1+S2,+∈{<+,+>},的集成或結(jié)合時(shí)，在集成后的規(guī)范S中處于主導(dǎo)地位的S1或S2，稱為該特性集成的框，另一方稱為該特性集成的核.如果不存在處于主導(dǎo)地位的規(guī)范，或?qū)τ赟=S1S2,則稱該集成是無(wú)框或無(wú)核的.

圖3(d)給出了特性集成的一般圖式表達(dá).圖3(c)表示以模型為核,結(jié)合環(huán)境的約束得到滿足語(yǔ)義保持的軟件實(shí)現(xiàn)的轉(zhuǎn)換關(guān)系.圖3(f)表示M1經(jīng)過(guò)兩次引入新的約束后得到M2

圖3 規(guī)范的轉(zhuǎn)換特性集成關(guān)系Fig.3 Property integration relationships of specification transformation

的轉(zhuǎn)換.圖中以實(shí)心菱形箭頭表示的是有核集成的框，核是用通常的三角箭頭表示的.

特性集成用來(lái)表示引入環(huán)境、平臺(tái)、模式、方面或其它模型等約束后得到的新的合成規(guī)范.

由于特性集成概念的存在，而且規(guī)范都是在相同抽象層次上的特性描述，因此,不引入新的規(guī)范而進(jìn)行的規(guī)范轉(zhuǎn)換沒(méi)有改變抽象的層次，是沒(méi)有實(shí)際本質(zhì)意義的.據(jù)此，本文以下關(guān)于轉(zhuǎn)換的討論主要都是關(guān)于或用于集成方面的.

定義15.分解/And分解(Decomposition).設(shè)M是規(guī)范S∈SP的特性集，S的分解表示為態(tài)射集合{S→aS1，…，S→aSn>0},其中,每一個(gè)Si也是規(guī)范,其特性集表示為Mi,并且滿足要求(MiM)(M1M2…Mn=M).

圖4(a)給出了規(guī)范分解的圖式表示.規(guī)范的分解抽象地描述了復(fù)雜的模型經(jīng)過(guò)分解和合成的軟件實(shí)現(xiàn).基于體系結(jié)構(gòu)規(guī)范的系統(tǒng)構(gòu)造就是經(jīng)過(guò)分解、成分構(gòu)造，而后成分合成而建立的.

圖4 規(guī)范的分解和選擇關(guān)系Fig.4 Decomposition and alternative of specification

定義16.選擇/Or選擇(Alternative).設(shè)M是規(guī)范S∈SP的特性集，S的選擇表示為態(tài)射集合{S→oS1，…，S→oSn>0},其中，每一個(gè)Si也是規(guī)范,并且滿足要求S=Si.

圖4(b)給出了規(guī)范選擇的圖式表示.“Or選擇”指任選其一的運(yùn)算，特指多個(gè)分支轉(zhuǎn)換關(guān)系中任選其中一個(gè)的設(shè)計(jì)選擇；對(duì)于各個(gè)分支，其實(shí)都是源規(guī)范的等價(jià)復(fù)制；所以，選擇等價(jià)于多個(gè)規(guī)范的復(fù)制.

由圖4可以看出，從范疇角度看，規(guī)范的分解和選擇都是類似椎(cone)[11]的概念.以下規(guī)范的合成則是類似余錐(cocone)[11]概念，它們的出現(xiàn)應(yīng)該看成是對(duì)規(guī)范分解和選擇的逆或?qū)ε歼\(yùn)算.對(duì)于建立完整的模型轉(zhuǎn)換概念這是必須的，這可以通過(guò)圖4中它們的出現(xiàn)情況說(shuō)明.

圖5 規(guī)范的選擇與合成關(guān)系舉例Fig.5 Example of alternative and composition

規(guī)范的合成有“And合成”和“Or合成”兩種類型.

定義17.And合成(And Composition).設(shè)M是規(guī)范S∈SP的特性集，S的And合成表示為態(tài)射集合{S1→acS，…，Sn→acS},其中,每一個(gè)Si也是規(guī)范，其特性集表示為Mi，并且滿足要求(M=M1M2…Mn).

定義18.Or合成(Or Composition).設(shè)M是規(guī)范S∈SP的特性集，S的Or合成表示為態(tài)射集合{S1→ocS，…，Sn→ocS},其中，每一個(gè)Si也是規(guī)范,其特性集表示為Mi,并且滿足要求(S=Si)(M=Mi).

“And合成”是“And分解”的對(duì)偶，“Or合成”是“Or選擇”的對(duì)偶，而且它們的出現(xiàn)應(yīng)該是成對(duì)的.圖4通過(guò)圖示說(shuō)明了這種對(duì)偶的出現(xiàn)，其中間節(jié)點(diǎn)所代表的規(guī)范可以進(jìn)一步發(fā)生其它轉(zhuǎn)換、分解和選擇.

圖4(a)還指出，分解和And合成的綜合轉(zhuǎn)換結(jié)果是(P1→S1Q1→T1M21)(P2→S2Q2→T2M22),這與轉(zhuǎn)換M1→TM2從結(jié)構(gòu)邏輯上是等價(jià)的.類似地，圖3(b)指出,選擇和Or合成的綜合轉(zhuǎn)換結(jié)果是(P1→S1Q1→T1M2)(P2→S2Q2→T2M2),這與轉(zhuǎn)換M1→TM2從語(yǔ)義邏輯上應(yīng)該是等價(jià)的.

圖5給出了一個(gè)規(guī)范經(jīng)過(guò)選擇和集成，而后又經(jīng)合成和集成所形成的轉(zhuǎn)換過(guò)程.M1→TM2= 其綜合轉(zhuǎn)換結(jié)果是((M11+N11)→F1Q1→T1M21)((M12+N12)→F2Q2→T2M22),這從語(yǔ)義邏輯上與轉(zhuǎn)換M1→TM2等價(jià).

定義19.規(guī)范范疇(SpecificationCategory). 規(guī)范范疇SC=，其中，S={S1,…,Sn>0}是非空規(guī)范集合,ST={轉(zhuǎn)換/t，分解/a,選擇/o,And合成/ac,Or合成/oc,集成/i,復(fù)制/d,不計(jì)類型/st }是態(tài)射類型集合，T={Si→stSj|Si,Sj∈S，st∈RT}是可為空的規(guī)范態(tài)射集合；其中，(規(guī)范復(fù)制)→d是一個(gè)等價(jià)態(tài)射.

可見(jiàn)，規(guī)范范疇也是一個(gè)類型化的范疇.

定義20.轉(zhuǎn)換路徑(Route of Transformation).對(duì)于規(guī)范M1和M2，如果可由M1經(jīng)歷一次或多次轉(zhuǎn)換態(tài)射推導(dǎo)而到達(dá)M2，則稱存在一條從M1到M2的轉(zhuǎn)換路徑R，并記為Rou∶M1M2.對(duì)于經(jīng)歷一次的轉(zhuǎn)換記為R∶M1→stM2.

定義21.路徑等價(jià)性(Equivalence of Route). 兩條從規(guī)范M1到M2的轉(zhuǎn)換路徑Rou1∶M1M2和Rou2∶M1M2是等價(jià)的，記為Rou1=Rou2，當(dāng)且僅當(dāng)轉(zhuǎn)換的結(jié)果都得到相等的特性集合.

考慮轉(zhuǎn)換的語(yǔ)義保持性，可以得到在語(yǔ)義保持意義下兩條從規(guī)范M1到M2轉(zhuǎn)換路徑的等價(jià)性定義.

使用以上對(duì)于分解,選擇和合成關(guān)系的簡(jiǎn)記形式,可以得到如下推論：

推論1. 對(duì)于規(guī)范M1,M2,S={S1,…,Sn>0}∈SP,以下態(tài)射關(guān)系集合所表達(dá)的轉(zhuǎn)換關(guān)系是等價(jià)的：

M1→TM2= {M1→aS1→acM2，…，M1→aSn→acM2}；

M1→TM2= {M1→oS1→ocM2，…，M1→oSn→ocM2}.

以上關(guān)系形成了發(fā)自M1到達(dá)M2的路徑束(bundle of route).如果壓縮這個(gè)束,以上關(guān)系可簡(jiǎn)記為：

M1→TM2= {M1→aS→acM2},當(dāng)S={S1,…,Sn>0}；

M1→TM2= {M1→oS→ocM2},當(dāng)S={S1,…,Sn>0}.

推論2. 對(duì)于規(guī)范M1,M2，S1={S11,…,S1n>0}，S2={S21,…,S2n>0}∈SP,以下態(tài)射關(guān)系集合所表達(dá)的轉(zhuǎn)換關(guān)系是等價(jià)的,其中指不計(jì)類型和次數(shù)的轉(zhuǎn)換.這里再次出現(xiàn)了路徑束及其壓縮現(xiàn)象：

M1→TM2= {M1→aS11S21→acM2，…，M1→aS1nS2n→acM2} = {M1→aS1S2→acM2}

M1→TM2= {M1→oS11S21→ocM2，…，M1→oS1nS2n→ocM2} = {M1→oS1S2→ocM2}

兩條不包含分解、選擇、合成、集成的從規(guī)范M1到M2的轉(zhuǎn)換路徑的等價(jià)性是容易判定的.使用以上的兩個(gè)推論可以得到類似，但可包含分解、選擇、合成、集成的兩條轉(zhuǎn)換路徑的等價(jià)性定義.因此有以下定義.

定義22.良定的規(guī)范范疇(Well-formed Specification Category).規(guī)范范疇SC=是良定的，當(dāng)且僅當(dāng)滿足以下條件：

1) 對(duì)于T所給出的規(guī)范態(tài)射,存在非空集合NSS和NFS,其中,s∈NS不存在任何s的前驅(qū)，而且s∈NF不存在任何s的后繼；

3) 轉(zhuǎn)換態(tài)射→a和→ac,→o和→oc必須分別先后成對(duì)出現(xiàn),其間可以存在其它轉(zhuǎn)換態(tài)射,單不存在與其它→a和→ac,→o和→oc對(duì)的交叉.一個(gè)良定的規(guī)范范疇可以記為WFSC=.

除具有多種態(tài)射類型外，良定的規(guī)范范疇是一個(gè)規(guī)范的偏序集合或DAG(Directed Acyclic Graph)圖.

4 應(yīng)用研究

本節(jié)通過(guò)一個(gè)關(guān)于學(xué)生信息管理的服務(wù)系統(tǒng)，作為實(shí)例闡述本文所提描述框架的應(yīng)用.應(yīng)用示例研究Student對(duì)象從基本規(guī)范到具體平臺(tái)(J2EE/.NET)下實(shí)現(xiàn)Grid展示的轉(zhuǎn)換.其轉(zhuǎn)換框架如圖6所示.考慮到篇幅限制，在示例中做了適當(dāng)簡(jiǎn)化.

圖6 應(yīng)用示例的轉(zhuǎn)換框架Fig.6 Transformation framework of the exmple

首先建立學(xué)生對(duì)象規(guī)范Student(圖7)，這是模型設(shè)計(jì)的基礎(chǔ)，根據(jù)前面定義，主要是屬性、動(dòng)作和公理的定義屬性有學(xué)號(hào)、姓名、出生日期等，而在動(dòng)作中示例中只給出了與出生日期有關(guān)的兩個(gè)動(dòng)作.相應(yīng)的公理則對(duì)其作了約束.

根據(jù)設(shè)計(jì)需求，Student對(duì)象規(guī)范實(shí)例需要展示在界面中，為此需要建立展示特性規(guī)范PresentPropertyofStudent(圖8)，該規(guī)范中定義了為滿足student規(guī)范實(shí)例在界面展示方面的需求，需要增加的屬性及動(dòng)作等.其中，屬性類型中的alias是別名，主要用于顯示時(shí)對(duì)屬性的提示說(shuō)明，length是最大允許長(zhǎng)度，這將決定屬性顯示時(shí)的布局空間限制.age是新增加的屬性，并指明是屬性birthday的導(dǎo)出項(xiàng)，由此將引起動(dòng)作的增加，getAge()是完成對(duì)屬性值的提取，而calculteAge()則描述導(dǎo)出語(yǔ)義，其中Current是指當(dāng)前日期.需要說(shuō)明的是calculteAge()被激發(fā)完成age屬性的重新計(jì)算后，所有已經(jīng)被調(diào)用的getAge()動(dòng)作需要重新激發(fā)，以完成age屬性值的同步.

圖7 學(xué)生對(duì)象規(guī)范Fig.7 Specification of student

圖8 展示特性規(guī)范Fig.8 Specification of presentive property

圖9 集成顯示特性的規(guī)范Fig.9 Specification of presentive property integrated

基本對(duì)象規(guī)范集成展示特性規(guī)范會(huì)形成適合界面展示方面需求的規(guī)范，此規(guī)范將作為界面展示轉(zhuǎn)換的設(shè)計(jì)基礎(chǔ).根據(jù)前面集成定義，完成StudentPresentPropertyofStudent計(jì)算將很容易得到集成顯示特性的學(xué)生規(guī)范IntegratedStudent(圖9).需要說(shuō)明的是由于age是birthday的導(dǎo)出項(xiàng)，在集成后的公理中增加了setBirthday(d)=> calculteAge()，語(yǔ)義為出生日期的設(shè)置將會(huì)引起年齡的重新計(jì)算.

設(shè)計(jì)需求表明，最終呈現(xiàn)在界面上的將是對(duì)象匯集，而對(duì)象匯集具有其特殊的結(jié)構(gòu)和操作特性，為此建立匯集特性規(guī)范模板