基于AOP的契約定義及其與JML契約的轉(zhuǎn)換

張 進，何成萬，石 尤

武漢工程大學計算機科學與工程學院，湖北 武漢430205

契約式設(shè)計（design by contract，DbC），又叫合同設(shè)計方法，可以用于確保程序的準確性和提高程序的可靠性，它是基于Hoare的公理化證明方法而開發(fā)的設(shè)計思想［1］?；诤贤拈_發(fā)主要是通過在程序模塊中添加前提條件、后置條件和不變量來為模塊設(shè)計契約［2］。前提條件描述一個模塊對調(diào)用該模塊人員提出的要求，調(diào)用此模塊之前必須滿足該模塊的前提條件。后置條件描述的是調(diào)用者在調(diào)用某模塊之后應(yīng)該滿足的條件。不變量是對于整個模塊而言，不變量必須在模塊執(zhí)行前后被滿足。在面向?qū)ο蟮脑O(shè)計中使用合同編程的思想，形成了各種支持契約式的語言，如Eiffel、Larch、Java建 模 語 言（java modeling language，JML）、還有Microsoft.Net平臺上的SPEC#等。其中，埃菲爾語言是最著名的規(guī)范語言［3］。

面向方面編程（aspect-oriented programming，AOP）通過封裝橫切關(guān)注點的思想為解決合同編程中所出現(xiàn)的代碼交織等問題提供了很好的解決方案，并且，AOP的語言結(jié)構(gòu)與契約之間也有著自然的對應(yīng)關(guān)系［4］，當不變式以及前置條件和后置條件均看成橫切關(guān)注點，AOP就可以很容易地完成它們與其他功能模塊之間的相互分離，使得開發(fā)人員可以在獨立的編織器模塊中實現(xiàn)和編寫這些模塊的功能，并以較為靈活的方式調(diào)用它們［5］。AOP的這些特性正好可以彌補合同編程的缺陷，所以，在面向?qū)ο笤O(shè)計中使用AOP技術(shù)來支持合同設(shè)計是一個增強軟件系統(tǒng)可靠性的新方法［6-7］。

但是，作為一種形式化的方法，基于AOP的契約很難執(zhí)行。此外，若用手動方法將基于AOP的契約轉(zhuǎn)換為可執(zhí)行程序會導(dǎo)致性能下降和難以維護等問題。

JML作為Java的注釋語言同樣允許規(guī)范，而且相關(guān)工具也很成熟。因此，本文分別討論了兩種語言，提出了一種基于AOP的契約定義的方法，并且給出了實例，本文還提出了一種將高抽象層次的基于AOP的契約規(guī)范翻譯為低抽象層次的JML規(guī)范的策略。目標是使用現(xiàn)有的基于JML的工具來驗證基于AOP的契約代碼。

1 國內(nèi)外相關(guān)工作的比較分析

對于面向方面編程和JML契約有很多研究者進行了研究，Rebêlo［8］曾在一篇論文中提過一種使用AspectJ來實現(xiàn)JML的方法，他提到使用AspectJ來實現(xiàn)一個新的JML編譯器，它生成一個符合檢測的字節(jié)碼，同時使用Java SE和Java ME應(yīng)用程序。并進行了比較研究來證明該編譯器生成的最終代碼的質(zhì)量，將代碼的大小與現(xiàn)有JML編譯器生成的代碼進行比較。此外，還評估了在Java應(yīng)用程序中實現(xiàn)JML斷言所需的額外代碼量。結(jié)果表明，該編譯器生成的代碼大小的開銷非常小，這對Java ME應(yīng)用程序至關(guān)重要。而本文的工作是用AOP來定義契約合同，然后根據(jù)定義的基于AOP的契約與JML契約之間的映射關(guān)系來介紹一種進行基于AOP的契約與JML契約相互轉(zhuǎn)換的模型策略。

Smith［9］介紹了一種將橫切特征表示為邏輯不變量，然后生成由手動編寫的方面得到的代碼的方法，并舉了各種例子說明了不變方法。該方法的關(guān)鍵思想是利用不變量捕獲方面的意圖。方面編織是通過在基本代碼的適當位置生成和插入代碼片段來保持不變的過程。在這種方法中，切入點規(guī)范是從不變量派生出來的，它描述了可能破壞不變量的一組代碼點。對于代碼中的每一個這樣的中斷點，維護代碼的規(guī)范是從不變式中派生出來的。與本文研究不同的是本文直接用AOP語言來描述契約合同，而不是進行方面編織。

Carr［10］提出了一種通過自動代碼將靜態(tài)分析結(jié)果應(yīng)用于現(xiàn)有代碼的新工具（code contracts bot，CCBot），CCBot使用方法前置條件，后置條件和對象不變量來檢測代碼，這些不變量在運行時或靜態(tài)使用靜態(tài)合同檢查器檢測故障。程序員需要執(zhí)行的唯一配置是為CCBot提供她想要檢測的代碼的文件路徑。這使程序員可以輕松地采用基于契約的靜態(tài)分析。如果原始代碼確實如此，CCBot的代碼檢測版本可以保證編譯。此保證意味著程序員可以立即部署或測試已檢測的代碼，無需額外的手動操作。插入的契約可以檢測常見錯誤，例如空指針解引用和超出范圍的數(shù)組訪問。本文研究的是將基于AOP契約轉(zhuǎn)換為JML契約，然后通過jmldoc來生成帶有JML注釋的文檔，從而實現(xiàn)將JML注釋自動插入到Java代碼中。

徐倩穎［11］提出了面向方面編程領(lǐng)域的一種新型設(shè)計模式：方面橋模式，該模式解決了構(gòu)件與行為模式間的耦合問題，體現(xiàn)了“高層分離，低層耦合”的原則。在該模式中，行為模式是通過抽象化方面來表現(xiàn)的，主要是對接口進行模塊化。而本文的研究是對契約進行模塊化，利用AOP語言來定義基于AOP的契約，從而實現(xiàn)契約的重用。

2 基于AOP的契約定義

2.1 AOP-DbC的對應(yīng)關(guān)系

契約的基本內(nèi)容包括：

前置謂詞：描述一個模塊對調(diào)用該模塊的人員提出的要求，調(diào)用此模塊之前必須滿足該模塊的前提條件。

合法的輸入：輸入的格式和取值是合法的。

期望的輸出：返回給用戶的結(jié)果。

后置謂詞：不管某類操作的執(zhí)行過程如何，在其終結(jié)之后必須滿足后置條件

不變式：在執(zhí)行某個操作之后變量保持不變。

圖1所展示的是契約式開發(fā)的一般邏輯。

DbC與AOP機制提供的語言結(jié)構(gòu)，諸如連接點、切入點以及通知等有著直接的對應(yīng)關(guān)系，使用before通知檢查前置條件，必須在執(zhí)行某個切入點確定的方法之前被檢查，而使用after通知檢查后置條件，必須在方法執(zhí)行之后進行檢查。同時使用before和after通知或者使用around通知檢查不變式，必須在方法執(zhí)行前后進行檢查。當前的研究領(lǐng)域不是偏重于下層的編碼細節(jié)，就是偏重于并不是為AOP專門設(shè)計的對象約束語言（object constraint language，OCL）等契約語言，所以，目前并沒有給出一個絕對的AOP-DbC的對應(yīng)關(guān)系。本文圖2給出了AOP和DbC之間的一個對應(yīng)關(guān)系。

圖1契約式開發(fā)的流程圖Fig.1 Flowchart of contract development

圖2 AOP與DbC的對應(yīng)關(guān)系Fig.2 Corresponding relationship between AOP and DbC

將非功能代碼（即非斷言所需的代碼）與業(yè)務(wù)邏輯代碼兩者混合起來，這種使用斷言機制支持契約的一種方法，會造成代碼糾纏。如果目的是為了分離關(guān)注點，從而達到靈活而透明的特點，那么面向方面編程則是最佳選擇［12］。前置謂詞、后置謂詞和不變式常出現(xiàn)于應(yīng)用程序的各個模塊中，在某種程度上與應(yīng)用程序代碼相混合，可以看作是橫切關(guān)注點的表現(xiàn)。AOP的目標就是讓開發(fā)人員可以在獨立的模塊中單獨編寫這些功能，然后自然地應(yīng)用它們。

AOP可以將橫切關(guān)注點模塊化［13］，而且DbC的實現(xiàn)也是橫切的。JML無法編寫單個前置和后置條件，并將其應(yīng)用于特定類型的多種方法，只能在每個方法中單獨添加，而這種前置或后置條件通常必須在幾種方法中重復(fù)和分散。

另一方面，目前存在的用于靜態(tài)分析的工具通常都需要很多程序員工作［14］。在大型代碼庫中，靜態(tài)分析工具會產(chǎn)生數(shù)千個警告，期望用戶查看如此龐大的列表并手動對每個警告進行更改是不現(xiàn)實的［15］。減少警告數(shù)量的一種方法是添加注釋，通常，注釋可能會禁用某些消息，指定程序的預(yù)期行為，或啟用/禁用某些代碼的分析。這些手動注釋在小例子中是可管理的，但是從完全未注釋的代碼庫開始時則不適用于大型代碼庫。自動插入合同而不是顯示警告列表，有兩個可用性優(yōu)勢，可以減少程序員所需的工作量。1）程序員可以使用熟悉的工具查看上下文的合同。2）接受或測試其代碼的修改版本，無需任何手動步驟。

2.2 前置條件的AOP定義

用before通知與方法的前置謂詞相對應(yīng)，圖3是前置謂詞的定義。

圖3前置條件的定義Fig.3 Definition of preconditions

在圖3中，pointcut表示方法的切入點，用來指定所選連接點中的關(guān)注，args表示方法調(diào)用的參數(shù)，如果不滿足前置條件，程序拋出異常。

2.3 后置條件的AOP定義

用after通知與方法的后置謂詞相對應(yīng)，圖4是后置謂詞的定義。

圖4后置條件的定義Fig.4 Definition of postconditions

在圖4中，pointcut表示方法的切入點，用來指定所選連接點中的關(guān)注，target表示目標對象，如果不滿足后置條件，拋出異常。

2.4 不變量的AOP定義

采用around通知對應(yīng)不變量，圖5是不變量的定義。

在圖5中，pointcut表示方法的切入點，用來指定所選連接點中的關(guān)注，target表示目標對象，args表示方法調(diào)用的參數(shù)，如果不滿足不變量，程序便會拋出異常。

圖5不變量的定義Fig.5 Definition of invariants

2.5 實例

AOP有著將橫切關(guān)注點模塊化的特點，而契約的約束條件如前置條件、后置條件、不變量約束可以看作橫切關(guān)注點，因此AOP可以將這些約束條件封裝成方面，與業(yè)務(wù)邏輯代碼分離。然后使用連接點、切入點來指定即將檢查的契約代碼的具體位置，并在相應(yīng)的before或者after以及around通知中定義契約的內(nèi)容。以邊界判斷為例，圖6是用AOP的方式實現(xiàn)邊界判斷的契約檢查。

從圖6可以看出，在PointBoundsPreCondition方面中，聲明了一個before通知，用于修改類Point的setX方法的行為。before通知可以應(yīng)用于每個連接點，args關(guān)鍵字表示方法調(diào)用的參數(shù)。在PointBoundsPostCondition方面中，聲明了一個normal after通知，該通知修改類Point的setX方法的行為。after通知可以應(yīng)用于每個連接點，target和args關(guān)鍵字表示目標對象和方法調(diào)用的參數(shù)。在PointBoundsInvariant方面中，它聲明了一個around通知來修改類Point的setX方法的行為。在每個連接點之前和之后檢查不變量，target和args關(guān)鍵字表示目標對象和方法調(diào)用的參數(shù)。如果x大于MIN_X，小于MAX_X，則執(zhí)行語句proceed（p，x）；另一方面，在else子句中，通知直接調(diào)用setX方法。一般情況下，一旦契約不能被滿足，程序就會拋出異常或直接退出程序。

圖6邊界判斷的基于AOP的契約檢查Fig.6 AOP-based contract checking for boundary determination

3 AOP契約到JML契約的轉(zhuǎn)換方法

3.1 JML語法

JML是一種通用規(guī)范建模語言，是面向Java的行為接口規(guī)范語言（behavior interface specification language，BISL）。它主要用于描述基于Java的調(diào)用模型的使用行為和詳細的模型設(shè)計。

JML規(guī)范是基于埃菲爾的DbC的思想。調(diào)用方有義務(wù)確保方法的先決條件是正確的，如果先決條件為false，則調(diào)用方與其被調(diào)用方之間的契約將不再有效。JML遵循BISL的形式化語義，繼承DbC的可執(zhí)行能力。

除了DbC中定義的前置條件和后置條件以及不變量外，JML還有許多其他類型的約束，這些約束增強了JML的驗證和調(diào)試機制。圖7顯示了含有JML注釋的具體Java代碼，JML注釋通過/*@和@*/來表示。

圖7 JML注釋的模板Fig.7 Template for JML annotations

目前，許多JML工具已經(jīng)成熟，如運行時斷言、jmlUnit和JMLAutoTest。使用這些 工具，JML規(guī)范可以轉(zhuǎn)換為可執(zhí)行代碼，然后利用運行時斷言進行檢查。除此之外，不僅能利用JML工具自動生成測試框架，還可以自動生成測試用例。

3.2 轉(zhuǎn)換策略

基于AOP的契約定義將前置條件、后置條件以及不變量封裝，有助于重用，但也有一定的缺陷性。而將基于AOP的契約定義轉(zhuǎn)換為JML契約，自動生成注釋加入到每個方法之內(nèi)，可以減少程序員的工作量，本文提出了一種兩者之間轉(zhuǎn)換的模型策略，如圖8所示。

從圖8中可以看出，本文是將基于AOP的契約與JML契約的轉(zhuǎn)換實現(xiàn)為一個插件工具（虛線框部分），該插件利用Java的反射機制來調(diào)用翻譯器進行兩種契約之間的轉(zhuǎn)換，而插件的用戶界面是用Window Builder和Java Swing實現(xiàn)的。

圖8基于AOP的契約和JML契約轉(zhuǎn)換的模型Fig.8 Model of conversion between AOP-based contract and JML contract

3.3 從基于AOP的契約類型到JML類型的映射

3.3.1 基本數(shù)據(jù)類型基于AOP的契約與JML契約之間最基本的映射是數(shù)據(jù)類型之間的映射。由于JML是針對Java定制的，而AOP與Java的實現(xiàn)相同。因此，在基本數(shù)據(jù)類型上，AOP與JML有著直接的對應(yīng)關(guān)系，兩種語言都主要包括int（整型）、double（雙精度浮點型）、boolean（布爾型）、char（字符串型）等基本數(shù)據(jù)類型。

3.3.2 運算符對于比較運算符，AOP和JML同樣對應(yīng)的都是Java類型，主要包括：==、！=、＜、＞、＜=、＞=等。但是二者在邏輯運算符上稍有不同，AOP和JML兩種語言在邏輯運算符上的映射關(guān)系如表1所示。

表1邏輯運算符Tab.1 Logical operators

3.3.3 集合類型Java最核心的3種集合類型分別是set（集）、list（列表）、map（映射）。JML定義了對應(yīng)的模型種類來表示各種不同的Java類的集合，分為對象集合和值集合，都實現(xiàn)了JMLCollection接口。對象集合中元素是對象的引用，并不關(guān)心對象的值。對象集合分為JMLObjectSet，JMLObjectBag，JMLObjectSequence 3種。值集合分為JMLValueSet，JMLValueBag，JMLValueSeque-nce 3種，值集合中的元素存儲的是對象的值。集合類型的對應(yīng)關(guān)系如表2所示。

表2集合類型的映射Tab.2 Mapping of collection types

3.3.4 約束規(guī)范的映射基于AOP的契約與JML契約在前置條件和后置條件以及不變量約束上均存在著一定的映射關(guān)系，使得2種契約之間的轉(zhuǎn)換成為可能，2種契約的元素之間的對應(yīng)關(guān)系如表3所示。

表3約束規(guī)范的元素之間的映射Tab.3 Mapping between elements of constraint specification

4 結(jié)論

基于AOP的契約可以將方法的前置條件、后置條件以及類不變式封裝，實現(xiàn)契約的模塊化處理，解決代碼糾纏問題。它與JML相似，但是各有優(yōu)缺點，JML具有更多的驗證特性。

本文分析了兩種不同抽象層次的規(guī)范語言：基于AOP的契約和JML契約。提出了一種基于AOP的契約與JML契約之間的轉(zhuǎn)換策略，并給出了基于AOP的契約與JML契約轉(zhuǎn)換之間的映射關(guān)系，使約束規(guī)范能夠更具體地指導(dǎo)后續(xù)的軟件開發(fā)。作為未來的工作，希望構(gòu)建一個框架來支持基于AOP的契約到JML契約的自動化轉(zhuǎn)換。