基于契約式設(shè)計的VeriJava編程語言設(shè)計

戴 維 標(biāo)

(鹽城工學(xué)院繼續(xù)教育學(xué)院，江蘇鹽城 224051)

基于契約式設(shè)計的VeriJava編程語言設(shè)計

戴 維 標(biāo)

(鹽城工學(xué)院繼續(xù)教育學(xué)院，江蘇鹽城 224051)

契約式設(shè)計是一種以Java語言為主流編程的技術(shù)手段，無論是在VeriJava編程語言程序開發(fā)中，還是在C++、S#等語言開發(fā)中，都被程序開發(fā)者廣泛使用.對VeriJava編程語言以契約式設(shè)計理論的程序設(shè)計進(jìn)行分析研究，將契約式設(shè)計理念引入到面向?qū)ο缶幊碳夹g(shù)開發(fā)中,從而實現(xiàn)契約的編寫與程序分離.

契約式設(shè)計理念；VeriJava編程語言設(shè)計；Java語言

契約式設(shè)計是指面向?qū)ο蟪绦蛑械念惻c客戶之間關(guān)系的一種形式化約定，主要包括前置條件、后置條件和不變式，在面向?qū)ο蟪绦蛑校挥忻鞔_了定義模塊之間的權(quán)利和職責(zé)，才能構(gòu)建高質(zhì)量、高可靠性的大型軟件系統(tǒng)，本文則通過設(shè)置契約來約束程序行為的新型語言系統(tǒng)——VeriJava，從而實現(xiàn)VeriJava程序的動態(tài)檢查.

1 契約式設(shè)計理論分析

在面向?qū)ο蟪绦蛑校跫s式設(shè)計要求客戶與提供者之間需遵循契約的規(guī)定[1]，其明確定義模塊之間的權(quán)利者職責(zé)，主要包括前置條件、后置條件和不變式，前置和后置條件都是針對某個方法的，即前置條件(precondition)必須滿足該方法被調(diào)用之前的條件，而后置條件(postcondition)必須滿足該方法被調(diào)用之后的條件，然而，不變式(invariant)是針對類的，其主要描述這個類的全局屬性，并且類的所有調(diào)用方法都必須滿足不變式.

分析契約式設(shè)計理論，是一種構(gòu)建高可靠軟件并將面向?qū)ο蟪绦蛑械念惣翱蛻糁g的關(guān)系作為一種形式化約定的系統(tǒng)化方法，然而，在形式化的基礎(chǔ)上，其需要明確類及客戶之間的權(quán)利和職責(zé)，而類及客戶模塊之間定義的約定則被稱為“契約”.為了構(gòu)建高質(zhì)量、可靠性的軟件系統(tǒng)，在實踐中，還需要使用規(guī)范說明(specification)，為系統(tǒng)化的測試和排錯提供良好的基礎(chǔ)，一般要求每一單元都要使用一個規(guī)范說明.在程序開發(fā)中使用規(guī)范說明，不僅可以為程序開發(fā)人員提供參考，也可以通過靜態(tài)驗證的定理證明來確保程序的正確性，因此，在程序開發(fā)中引入契約式設(shè)計理論，不僅可以讓人們更好地理解面向?qū)ο蟮姆椒ê蛙浖?gòu)造，還可以更好地理解和控制繼承機(jī)制，是一種安全、高效處理程序異常的技術(shù)[2].

2 VeriJava編程語言概述

在面向?qū)ο筌浖绦蜷_發(fā)中，最為直觀、有效的形式屬于程序開發(fā)人員直接編寫契約.由于Java是一種面向?qū)ο蟮母呒壵Z言，雖然其具有實現(xiàn)多個接口、動態(tài)分配方法等特性，但其類只能從一個父類進(jìn)程，而VeriJava是Java編程語言的拓展語言，VeriJava編程語言設(shè)計的主要目標(biāo)是令Java語言通過支持契約具有可驗證性，這就需要提供靜態(tài)驗證、動態(tài)檢查的程序接口，并且需要為VeriJava提供基本的編輯器和動態(tài)驗證器等工具支持.圖1為 VeriJava 語言系統(tǒng)的整體架構(gòu)圖，從圖中可以看出，VeriJava 語言系統(tǒng)的基礎(chǔ)架構(gòu)屬于VeriJava 語言的定義與規(guī)范，通過構(gòu)建編譯器和利用動態(tài)檢查工具作為整個面向?qū)ο缶幊痰募夹g(shù)支撐，對基本的類進(jìn)行封裝，通過對程序設(shè)計進(jìn)行靜態(tài)驗證，這樣就可以通過定理證明對基于契約式設(shè)計編寫的程序進(jìn)行驗證[3].

圖1 VeriJava 語言系統(tǒng)的整體架構(gòu)

3 VeriJava語言程序設(shè)計分析

3.1 在VeriJava程序設(shè)計中契約條件的支撐

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

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

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

=???

= < REQUIRES_STATEMENT >

=|

=

= requires

= ensures

= signals

= modifies

= ?

?

= $return

= old( )

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

例如，下面則是VeriJava 語言編寫的代碼，進(jìn)而說明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) //構(gòu)造器對非空類型的初始化

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語言編程設(shè)計中的動態(tài)檢查分析

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

圖2 契約組件設(shè)計與實現(xiàn)架構(gòu)圖

4 結(jié)束語

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

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

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

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

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

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

(責(zé)任編輯 印亞靜)

2014-09-26

戴維標(biāo)，男，江蘇射陽人，鹽城工學(xué)院繼續(xù)教育學(xué)院技師.

TP313

A

1671-1696(2014)11-0015-03