基于契約式設計的VeriJava編程語言設計

戴 維 標

(鹽城工學院繼續教育學院，江蘇鹽城 224051)

基于契約式設計的VeriJava編程語言設計

戴 維 標

(鹽城工學院繼續教育學院，江蘇鹽城 224051)

契約式設計是一種以Java語言為主流編程的技術手段，無論是在VeriJava編程語言程序開發中，還是在C++、S#等語言開發中，都被程序開發者廣泛使用.對VeriJava編程語言以契約式設計理論的程序設計進行分析研究，將契約式設計理念引入到面向對象編程技術開發中,從而實現契約的編寫與程序分離.

契約式設計理念；VeriJava編程語言設計；Java語言

契約式設計是指面向對象程序中的類與客戶之間關系的一種形式化約定，主要包括前置條件、后置條件和不變式，在面向對象程序中，只有明確了定義模塊之間的權利和職責，才能構建高質量、高可靠性的大型軟件系統，本文則通過設置契約來約束程序行為的新型語言系統——VeriJava，從而實現VeriJava程序的動態檢查.

1 契約式設計理論分析

在面向對象程序中，契約式設計要求客戶與提供者之間需遵循契約的規定[1]，其明確定義模塊之間的權利者職責，主要包括前置條件、后置條件和不變式，前置和后置條件都是針對某個方法的，即前置條件(precondition)必須滿足該方法被調用之前的條件，而后置條件(postcondition)必須滿足該方法被調用之后的條件，然而，不變式(invariant)是針對類的，其主要描述這個類的全局屬性，并且類的所有調用方法都必須滿足不變式.

分析契約式設計理論，是一種構建高可靠軟件并將面向對象程序中的類及客戶之間的關系作為一種形式化約定的系統化方法，然而，在形式化的基礎上，其需要明確類及客戶之間的權利和職責，而類及客戶模塊之間定義的約定則被稱為“契約”.為了構建高質量、可靠性的軟件系統，在實踐中，還需要使用規范說明(specification)，為系統化的測試和排錯提供良好的基礎，一般要求每一單元都要使用一個規范說明.在程序開發中使用規范說明，不僅可以為程序開發人員提供參考，也可以通過靜態驗證的定理證明來確保程序的正確性，因此，在程序開發中引入契約式設計理論，不僅可以讓人們更好地理解面向對象的方法和軟件構造，還可以更好地理解和控制繼承機制，是一種安全、高效處理程序異常的技術[2].

2 VeriJava編程語言概述

在面向對象軟件程序開發中，最為直觀、有效的形式屬于程序開發人員直接編寫契約.由于Java是一種面向對象的高級語言，雖然其具有實現多個接口、動態分配方法等特性，但其類只能從一個父類進程，而VeriJava是Java編程語言的拓展語言，VeriJava編程語言設計的主要目標是令Java語言通過支持契約具有可驗證性，這就需要提供靜態驗證、動態檢查的程序接口，并且需要為VeriJava提供基本的編輯器和動態驗證器等工具支持.圖1為 VeriJava 語言系統的整體架構圖，從圖中可以看出，VeriJava 語言系統的基礎架構屬于VeriJava 語言的定義與規范，通過構建編譯器和利用動態檢查工具作為整個面向對象編程的技術支撐，對基本的類進行封裝，通過對程序設計進行靜態驗證，這樣就可以通過定理證明對基于契約式設計編寫的程序進行驗證[3].

圖1 VeriJava 語言系統的整體架構

3 VeriJava語言程序設計分析

3.1 在VeriJava程序設計中契約條件的支撐

VeriJava編程語言是一種作為擴展Java語言支持契約式設計的語言系統.契約分為類、非空類型及方法等三種契約類型.第一，方法契約類型，主要表達語言執行前后的狀況，其局限于它所限定的某個特定方法.第二，類契約，契約的作用范圍為整個類的范圍，即在對象生存周期中需要定義特殊的時間點及常量契約的校驗；第三，非空類型契約，主要針對契約中的特殊條件的契約類型，在契約規定中，一般要求非空類型契約的類的初始化值需要有參數，而不能為空，并且在類聲明中，也需要有某種形式的域，除特殊對象外，一般類的創建都需要采用 new操作符后面加上構造類型的模式來實現，在提供構造器過程中，必須提供初始化參數，這樣才能在編譯過程中作用于構造器的約束[4].

3.2 VeriJava編程語言詞法、語法、語義定義

通過在原有Java支持的契約條件的基礎上來制定出VeriJava語言系統的基本規范，其中，定義詞法、語法和語義是語言系統的基礎，在定義語言，最為規范的則是利用BNF范式來定義詞法和語法，BNF范式是支持以迭代的方式進行驗證.由于VeriJava設計支持方法契約、類契約和非空契約等三個方面的契約條件，其不僅為對象中的屬性增加約束，也為方法增加了以前置和后置條件為基礎的契約，針對VeriJava編程語言的定義，其主要是在Java語法特性上進行定義，在語法定義中通常采用遞歸定義的方式，其是BNF范式中的方法，如方法契約的定義：

=???

= < REQUIRES_STATEMENT >

=|

=

= requires

= ensures

= signals

= modifies

= ?

?

= $return

= old( )

一般情況下，語義定義的說明需要利用所有契約的通式進行說明，并且所有的契約條件都是由布爾表達式構成的，包括前置條件，后置條件及常量等，所以，利用Java布爾表達式進行語言編寫，在包含多個條件的情況下，可以利用&符號將多個條件連接.從方法契約定義中，可以知道方法契約主要由前置條件、后置條件和框架條件構成，在不制定的情況下，則說明無需校驗滿足契約.在程序編寫中，在契約方法無副作用情況下，VeriJava允許利用含有契約的方法來進行契約的編寫，若利用VeriJava語言本身的表達式來編寫契約，則可能會出現校驗契約表達式出現錯誤的情況.一般情況下，除private方法之外，方法契約都可以使用其他方法.另外，在方法契約中，還包括方法簽名 、方法聲明等語義定義，引入方法契約后，這就需要對方法名的定義進行相應的修改，即方法聲明之后，需要在之前加入方法契約[5].

例如，下面則是VeriJava 語言編寫的代碼，進而說明VeriJava的語言特性：

Package st.cee.java.aa;

Class Company{

Invariant employ Number>0; //常量

!String company Name； //非空類型聲明

! Int employ1; //非空類型

Public Company() company Name=“Example Company”(employ Number=50) //構造器對非空類型的初始化

Public void recruit (int new Comer)

Requires new Comer>=0 //前置條件

Ensures old (employ Number)

Modifies this.employ Number{

employ Number+=new Comer;

}

}

3.3 在VeriJava語言編程設計中的動態檢查分析

分析契約校驗的類型主要分為靜態和動態兩種契約檢查類型，針對靜態的契約檢查，由于靜態驗證包含在靜態編譯器的范圍之內，這就需要利用編譯器來完整契約校驗.因此，本文則重點分析動態的執行期契約檢查.動態檢查主要是利用契約動態檢查的工作原理進行某個轉換程序的轉換，通過將契約條件轉換為符合面向對象的Java語句，并對斷言語句進行判斷，若契約條件檢驗失敗，系統將以異常的形式將錯誤信息報告給程序開發人員.在動態檢查中，采用面向方面的編程的實現方式，其簡稱為AOP，將面向方面編程的實現方式應用在動態檢查中，不僅可以充分體現出代碼的靈活性，也可以明確表達設計的程序與類中組件之間契約.圖2表示基于AOP的契約動態檢查，分析面向方面的編程(AOP)的概念，對于AOP中的切面(Aspect)，其是對象操作過程中權限檢查、日志、事物處理等截面，對于AOP中的Advice，則主要是對某個連接點所采用的處理邏輯，在Java領域中，最為成熟的則屬于Aspect技術.在契約動態檢查中，其主要發生在程序執行到某些特性的階段，契約動態檢查實際上是一種橫切關注點分離的方式.比如面向對象語言中某個對象的調用，在調用之前，首先應對契約中的前置條件、后置條件和常量進行校驗，程序開發人員可以在單獨的模塊中利用面向方面的編程技術來編寫語言，充分利用契約中的聲明條件.采用面向方面的編程技術，不僅優化了橫切關注點的建模，也方便程序開發人員對系統進行合理設計、理解和維護，提高代碼的產量和質量，使AOP技術更有益于實現追加的特性.

圖2 契約組件設計與實現架構圖

4 結束語

VeriJava是一種原有Java的拓展語言系統，通過構建全新的VeriJava語言系統來實現Java編程語言支持契約式設計，即在契約式設計理論下通過利用含有契約的方法進行編寫契約，當程序編寫完成后，采用基于AOP的契約動態檢查工具對編寫的代碼進行整合，使程序開發人員可以直接對程序進行動態驗證.

[1]顧毅.基于元數據的Java平臺契約式設計框架研究[D].上海：上海交通大學碩士學位論文,2008.

[2]陳平,夏敏.一種使用AspectJ技術的Java契約式編程語言模型[J].東北電力大學學報,2011(3).

[3]劉振安,王文濤.一種Java平臺上契約式語言的設計與實現[J].測控技術,2008(1).

[4]章程,趙建軍,沈備軍,等.支持契約式設計的Java靜態驗證器的研究[J].計算機應用與軟件,2008(5).

[5]何丹丹,王立娟,劉瑞杰.基于用例契約化的測試用例生成策略[J].西南師范大學學報(自然科學版),2013(11).

(責任編輯 印亞靜)

2014-09-26

戴維標，男，江蘇射陽人，鹽城工學院繼續教育學院技師.

TP313

A

1671-1696(2014)11-0015-03