基于AOP的契約定義及其與JML契約的轉換

張 進，何成萬，石 尤

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

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

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

但是，作為一種形式化的方法，基于AOP的契約很難執行。……