摘 要：形式化規(guī)格是保證所設(shè)計(jì)的系統(tǒng)具有較高的可信度和正確性的重要途徑，它涉及軟件生命周期的各個(gè)階段。從形式化規(guī)格到軟件編碼是軟件開發(fā)中的一個(gè)關(guān)鍵環(huán)節(jié)。在分析了規(guī)格化和高級語言之間的內(nèi)在關(guān)系的基礎(chǔ)上，概括了基于Object-Z規(guī)格到Java實(shí)現(xiàn)的幾條轉(zhuǎn)換機(jī)制，并運(yùn)用案例研究來說明這些機(jī)制。

關(guān)鍵詞：軟件體系結(jié)構(gòu)；形式規(guī)格；Object-Z；Java；轉(zhuǎn)換機(jī)制

中圖分類號：TP391.41

形式化規(guī)格是為目標(biāo)系統(tǒng)建立精確模型的過程，該模型的作用是為系統(tǒng)功能提供清晰的規(guī)格。規(guī)格是實(shí)現(xiàn)的終極參考，也是最后驗(yàn)證的基礎(chǔ)。

怎樣將面向?qū)ο蟮囊?guī)格描述轉(zhuǎn)換為高級語言代碼？怎樣驗(yàn)證實(shí)現(xiàn)代碼與原來的規(guī)格是否相符？以及怎樣驗(yàn)證這些代碼是否能完全滿足需求？這些都是以軟件體系結(jié)構(gòu)思想為指導(dǎo)的軟件工程所面對的和需要解決的關(guān)鍵問題。

本文從面向?qū)ο蟮幕咎卣鞒霭l(fā)，闡述了從Object-Z到Java的一般轉(zhuǎn)換機(jī)制。

1 Object-Z規(guī)格到Java的轉(zhuǎn)換機(jī)制

從Object-Z規(guī)格到Java的實(shí)現(xiàn)是一個(gè)逐步求精的過程，類、對象、屬性、方法和消息是Object-Z的基本特征，其求精過程需圍繞這些基本特征進(jìn)行，以類和對象等為轉(zhuǎn)換單元。

1.1 封裝的轉(zhuǎn)換機(jī)制——模塊法則

封裝是將抽象而來的數(shù)據(jù)和功能有機(jī)的結(jié)合，屏蔽其屬性和實(shí)現(xiàn)細(xì)節(jié)，使內(nèi)部數(shù)據(jù)的完整性得到充分保障。

人都有姓名和年齡等共同屬性，所以人都屬于一個(gè)基本的類Person，盡管具體對象的某些屬性會(huì)有所差異；對外，Person對象的內(nèi)部方法是透明的，而形式化規(guī)格相對抽象或簡單些。例如，在規(guī)格中不會(huì)直接說明獲取或修改某些屬性值的方法。Object-Z規(guī)格只封裝基本框架，在所用語言環(huán)境里實(shí)現(xiàn)細(xì)節(jié)。例如：應(yīng)該為外部設(shè)置讀取name屬性值的方法getName和修改其值的方法setName。精化過程如圖1所示。

模塊法則以類為轉(zhuǎn)換單元，基本屬性一般直接轉(zhuǎn)換；可見的屬性則應(yīng)補(bǔ)充調(diào)用和修改方法，外界通過這些方法獲得或改變相應(yīng)屬性的值。

在Object-Z規(guī)格中，一旦某個(gè)類是通過繼承另外一個(gè)類的規(guī)格得來，只需將這個(gè)父類納入到這個(gè)子類的聲明中。依據(jù)Java的語法規(guī)則，類的繼承在實(shí)現(xiàn)時(shí)適宜擴(kuò)展法則，也即在預(yù)定義好的類的基礎(chǔ)上產(chǎn)生一個(gè)子類，該子類除擁有父類的所有特征，還可以加入自己的專有屬性。

圖1 Person類精化過程圖

1.2 繼承的轉(zhuǎn)換機(jī)制——擴(kuò)展法則

實(shí)現(xiàn)時(shí)分兩次擴(kuò)展。在確定父類所在位置和包名后，通過關(guān)鍵字import指定將要從包中導(dǎo)入的父類。假設(shè)包x.model擁有Person類，則在定義Student類之前加上import x.model.Person代碼行。第二次擴(kuò)展時(shí)只要在聲明類的開始用extends關(guān)鍵字導(dǎo)入類名即可。實(shí)現(xiàn)Student類的主要代碼如下：

public void init{…} }類之間的節(jié)點(diǎn)連線可以表明繼承的等級。圖2中空心箭頭指向的節(jié)點(diǎn)是父類，childclass1～childclassn是其可能的子類。圖中示意了子類childclass1的代碼段，其他子類與之類似。

圖2 繼承的轉(zhuǎn)換機(jī)制

1.3 多態(tài)的轉(zhuǎn)換機(jī)制——還原法則

多態(tài)性允許對子類繼承過來的方法進(jìn)行重寫、重載和動(dòng)態(tài)連接。消息達(dá)到時(shí)對象對其做出自己的反應(yīng)。在Object-Z規(guī)格中，多態(tài)也有相似特性。

多態(tài)涵蓋了接口繼承。圖3中接口繼承用空心箭頭說明關(guān)系，通過函數(shù)重載的類，都將繼承這個(gè)接口。圖中用do anything示意需要完成的工作，在轉(zhuǎn)換實(shí)現(xiàn)時(shí)必須用能真實(shí)完成功能的代碼段。轉(zhuǎn)換機(jī)制看似簡單，但說明了這樣一個(gè)道理：可以通過分解和化小的辦法來解決復(fù)雜問題的實(shí)現(xiàn)。

圖3 多態(tài)的轉(zhuǎn)換機(jī)制

1.4 類的轉(zhuǎn)換機(jī)制——對應(yīng)法則

案例：16個(gè)小方塊（按鈕）組成4×4的棋盤，每個(gè)按鈕都只有實(shí)心或空心兩種狀態(tài)。單擊任意一個(gè)按鈕，消息會(huì)傳遞到被單擊的按鈕以及與它相鄰的按鈕，這些按鈕將切換狀態(tài)。開始時(shí)棋盤上的按鈕都是空心，游戲的目標(biāo)是使棋盤上所有的按鈕都是實(shí)心。圖4是棋盤可能的中間狀態(tài)。

（1）模塊初始化

用自然數(shù)0-15對按鈕進(jìn)行編號（如圖5所示）。

圖4 圖5

定義類型Posn==0..15，按鈕的鄰居關(guān)系則可以通過坐標(biāo)清楚的表達(dá)出來，關(guān)系neigh表明兩個(gè)按鈕的相鄰關(guān)系；全局類型Style定義按鈕的兩種可能狀態(tài)（Style：：== hollow|solid），每個(gè)類都可以利用它；兩者的規(guī)格如下：

Style類型的屬性style用來標(biāo)明按鈕當(dāng)前狀態(tài)，初始時(shí)是空心，某個(gè)按鈕的toggle操作被執(zhí)行時(shí)，它的這個(gè)屬性將在hollow和solid之間切換。類togglebutton沒有記錄按鈕位置的屬性，原因是按鈕不需關(guān)注自己的位置和鄰居。也即在這個(gè)抽象層面上，按鈕的形狀是非實(shí)質(zhì)的，在具體實(shí)現(xiàn)時(shí)按鈕才是真實(shí)的方塊，但與之前描述的功能和結(jié)構(gòu)之間沒有關(guān)聯(lián)。

（2）按鈕問題

按鈕問題通過ButtonPuzzle類規(guī)格，屬性board是聯(lián)系按鈕對象和對應(yīng)位置的全函數(shù)，即16個(gè)按鈕分別對應(yīng)16個(gè)位置。函數(shù)posn是一對一的部分入射函數(shù)（board的逆），用來求被擊按鈕在棋盤上的位置。toggleButtonAndNeighbours操作以按鈕對象（b？）為輸入，對它及它的每位鄰居進(jìn)行狀態(tài)切換。函數(shù)puzzleSolved求所有按鈕是否都是實(shí)心狀態(tài)。

注意：關(guān)系neigh被用來求按鈕b？的鄰居

顯然，按鈕問題對象既是系統(tǒng)對象，也是傳遞消息的過渡對象。單擊某個(gè)按鈕時(shí)，按鈕問題對象會(huì)向這個(gè)被單擊的按鈕的鄰居發(fā)送切換消息。但在這個(gè)模式中，按鈕并沒有直接提及任何其他的按鈕。

（3）類的轉(zhuǎn)換機(jī)制說明

通過Object-Z規(guī)格化的ToggleButton類可以被精化為Java相應(yīng)的類，它繼承了類庫canvas；用布爾型變量hollow來對應(yīng)規(guī)格中的style屬性，hollow的true和1值分別表示按鈕是空心或?qū)嵭?；定義方法toggle實(shí)現(xiàn)規(guī)格中的按鈕toggle操作；定義布爾型函數(shù)isSolid用來返回按鈕的狀態(tài)是否為實(shí)心。

然而在實(shí)現(xiàn)時(shí)，往往需要更多的編碼以實(shí)現(xiàn)規(guī)格化中沒有直接描述的方面。比如Object-Z并沒有規(guī)格按鈕的大小形狀，但在Java編碼時(shí)需要定義方法paint用以繪制48×48像素的實(shí)心或空心矩形按鈕。

實(shí)現(xiàn)ToggleButton時(shí)還需要定義一個(gè)對象變量mediator。當(dāng)鼠標(biāo)被按下時(shí)，方法mousepressed將以toggleButton自身作為參量，發(fā)送給mediator消息toggleButtonAndNeighbours，mediator再將消息toggle發(fā)送給按鈕自己以及按鈕的鄰居，從而觸發(fā)相關(guān)按鈕對象的切換事件。當(dāng)按鈕被創(chuàng)建時(shí)，由構(gòu)造函數(shù)給對象變量mediator賦值。這些在Object-Z規(guī)格中也沒用涉及。類ToggleButton的Java實(shí)現(xiàn)如下：

類的聚集和消息的傳遞與一般轉(zhuǎn)換機(jī)制不盡相同，它們都是相對復(fù)雜的過程。需要找出它們的一般規(guī)律，在實(shí)際工作中，按照這些一般規(guī)則，將復(fù)雜問題分解并化簡。例如有classA、classB和classC三個(gè)類，classA是classB的父類，classC是一個(gè)相關(guān)類。classB的參數(shù)Bvar是classC的一個(gè)對象；classB的bmethod1方法的參數(shù)是一個(gè)classC對象，且還調(diào)用從classA繼承過來的Amethod1方法；Amethod1的輸入是classA的對象，它還調(diào)用classC的Cmethod1函數(shù)，而其輸入變量是classB對象。classB的init和輸出結(jié)果等方法因?yàn)闆]有調(diào)用其他函數(shù)，都通過Amethodn抽象化（如圖6所示）。

圖6 類的轉(zhuǎn)換機(jī)制

1.5 對象的轉(zhuǎn)換機(jī)制——抽象具體化法則

類是抽象的，而對象是具體的。對象是依賴于類的調(diào)用而動(dòng)態(tài)存在，先有了類才能使抽象的類具體化，從而有了對象。下面仍以按鈕問題為例，繼續(xù)實(shí)現(xiàn)ButtonsPuzzle類，這一過程體現(xiàn)了對象是如何編碼實(shí)現(xiàn)的。

在Java編碼時(shí)，類ButtonsPuzzle通過繼承類庫中的Applet而來。其中的board變量與Object-Z規(guī)格中的board對應(yīng)，它是長度為16的數(shù)組，下標(biāo)標(biāo)記按鈕順序。init方法將為每個(gè)元素創(chuàng)建具體對象（按鈕），并確立了按鈕位置和數(shù)組元素之間的關(guān)系，按鈕的過渡對象是ButtonsPuzzle對象自身（this）。規(guī)格中用來選擇給定按鈕的鄰居的兩個(gè)變量buttons和posn，在實(shí)現(xiàn)時(shí)沒有按變量聲明，因?yàn)檫@種選擇直接由計(jì)算機(jī)系統(tǒng)進(jìn)行。舉例來說，規(guī)格中定義的關(guān)系neigh在Java中是通過neigh函數(shù)實(shí)現(xiàn)的，但是neigh規(guī)格僅僅簡單的表示兩個(gè)位置是否相鄰。規(guī)格中的逆函數(shù)posn與編碼中的posn函數(shù)對應(yīng)，都返回指定按鈕的位置（編號）。

實(shí)現(xiàn)的方法toggleButtonAndNeighbours與規(guī)格化中的名字一致。當(dāng)某按鈕收到toggle消息時(shí)，除了自己切換狀態(tài)外，還要使所有相鄰按鈕也發(fā)生切換；之后檢查目標(biāo)狀態(tài)是否達(dá)到；若目標(biāo)狀態(tài)已達(dá)，給出完成提示信息。檢查工作由布爾函數(shù)puzzleSolved完成。類ButtonsPuzzle的實(shí)現(xiàn)如下：

從同一個(gè)類具體化出來的多個(gè)對象也會(huì)有一些不同。因此，在研究對象和類等的實(shí)現(xiàn)時(shí)應(yīng)該綜合考慮，把它們孤立起來沒有意義。例如，類mainclass繼承類pclass而來，它的輸入變量為classA類型，而classA是一個(gè)相關(guān)類，對象的實(shí)現(xiàn)機(jī)制如圖7所示。

圖7 對象的轉(zhuǎn)換機(jī)制

2 結(jié)束語

通過分析面向?qū)ο缶幊痰姆庋b、多態(tài)、繼承等重要特點(diǎn)，研討了從Object-Z形式化規(guī)格到Java語言編碼實(shí)現(xiàn)的一般轉(zhuǎn)換原理，提出了幾條有效且可行的轉(zhuǎn)換機(jī)制，通過實(shí)例進(jìn)行了演示和說明。從形式化規(guī)格到高級語言實(shí)現(xiàn)這一過程是一個(gè)復(fù)雜工程，今后還將進(jìn)一步完善轉(zhuǎn)換機(jī)制，并開展轉(zhuǎn)換后的驗(yàn)證工作。

參考文獻(xiàn)：

[1]Duke R.，Rose G.Formal object-oriented specification using object-Z[M]. Macmillan press limited，2000.

[2]孫昌愛，金茂忠，劉超.軟件體系結(jié)構(gòu)研究綜述[J].軟件學(xué)報(bào)，2002，13（7）：1228-1237.

[3]陳琳琳，戎玫，張廣泉.體系結(jié)構(gòu)規(guī)格語言XYZ/ADL到UML的映射[J].計(jì)算機(jī)應(yīng)用，2006，26（2）.

[4]唐姍，趙文耘.基于反射的動(dòng)態(tài)軟件體系結(jié)構(gòu)實(shí)現(xiàn)[J].微電子學(xué)與計(jì)算機(jī)，2006，23（9）.

[5]李瑩.軟件工程形式化方法與語言[M].杭州：浙江大學(xué)出版社，2010.

[6]NASA JPL.Formal Methods Specification and Verification Guidebook for Software and Computer Systems[M].Pasadena，CA，USA，1-59，1995.

[7]Jonathan A.，Craig C.，and David N. Arch Java： Connecting Software Architecture to Implementation[C].Processing’s of the 24th.International Conference on Software Engineering，2002.

[8]Smith G.The Object-Z Specification Language-Advances in Formal Methods[M].Kluwer Academic Publishers，2000.

作者簡介：王志剛（1962.6-），男，湖南沅江人，教授，研究方向：軟件工程、計(jì)算機(jī)網(wǎng)絡(luò)。

作者單位：湖南師范大學(xué)數(shù)學(xué)與計(jì)算機(jī)學(xué)院，長沙 410081