Object—Z規(guī)格到實現(xiàn)機制探討

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

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

中圖分類號：TP391.41

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

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

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

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

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

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

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

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

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

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

圖1 Person類精化過程圖

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

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

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

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

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

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

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

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

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

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

（1）模塊初始化

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

圖4 圖5

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

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

（2）按鈕問題

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

注意：關系neigh被用來求按鈕b？的鄰居

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

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

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

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

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

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

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

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

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

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

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

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

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

2 結束語

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

參考文獻：

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

[2]孫昌愛，金茂忠，劉超.軟件體系結構研究綜述[J].軟件學報，2002，13（7）：1228-1237.

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

[4]唐姍，趙文耘.基于反射的動態(tài)軟件體系結構實現(xiàn)[J].微電子學與計算機，2006，23（9）.

[5]李瑩.軟件工程形式化方法與語言[M].杭州：浙江大學出版社，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-），男，湖南沅江人，教授，研究方向：軟件工程、計算機網(wǎng)絡。

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