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

[摘 要]：文章定義了VeriJava語言系統的語法和詞法，并將契約式設計條件實現，對于實踐而言，以ECLIPSE插件為基礎，簡要介紹了VeriJava開發工具包，實現了VeriJava程序利用開發工具即可創建。并在VeriJava插件工具包中集成了動態檢查工具，可動態檢查程序。

[關鍵詞]：編程 動態檢查 VeriJava 契約式設計

隨著網絡信息化及計算機技術的不斷飛躍發展，契約式設計理念被多種編程語言支持，其中，主流編程語言就是JAVA。為了使JAVA從語言級別對契約式設計形成支持，開發以契約編程為基礎的模式，在保留JAVA原有特性前提下，擴展JAVA語言，于是誕生了VeriJava。契約式設計科提高對軟件的可靠性。在契約式設計中，軟件系統作為互相交流的部件，而部件相互之間的義務被定義為契約。

一、契約式設計的定義及其對程序開發的意義

契約式設計是一種設計計算機軟件的方法，且構建的軟件具有高可靠性與高質量，該方法對軟件設計者提出要求，則為軟件組件定義接口，且該接口是可驗證、精確的、正式的。近些年來，無論是技術上還是理論上，契約式設計都取得了前所未有的成績，受到工業領域和學術界的廣泛關注，且契約式編程概念也隨之誕生。JAVA平臺也有了諸多不同的技術支持契約式技術，例如：JCONTRACTOR以及ICONTRACT等技術。將契約式設計引入程序中后，該設計的引入大幅增強了軟件系統完備性和充實性，可通過契約式設計的引入優點來了解其深遠意義。契約式設計不會混淆接口文檔，書寫清晰；可控制和減少調試產生的開銷，利用監測可將錯誤及時發現；分離常規應用與契約檢查，控制、降低測試成本；以契約式設計為基礎實現異常情況的有效、安全處理；使人更好了解及操控繼承機制；該設計能夠給軟件部件創建文檔；確保質量，并且為測試、除錯提供出高效率框架；深化軟件構造和面向對象方法的理解。

二、VERIJAVA 語言的設計、定義與特性

在對語義進行定義之前，應說明與契約條件相適用的通式，由布爾表達式構成常量、前置、后置這3種條件的。由框架條件、前置條件、后置條件共同構成了方法契約，方法契約由進行定義。若未指定三個元素，則說明無需對滿足契約的情況進行校驗。這樣定義的好處是為了在VeriJava中JAVA程序不會因契約不足而不合法。在限定程序行為的同時，VeriJava語言中的方法契約自身不會將程序的狀態改變。除了PRIVATE方法之外，方法契約適用于任何方法。通過擴展JAVA語言，VeriJava語言系統對語法和語義進行了全新定義，是契約式設計成為現實。在VeriJava語言的規定下，契約成為接口和類的一部分，布爾表達式能夠實現契約條件的編寫。對于原有的JAVA語法語義，VeriJava沒有進行改寫，這樣設計時考慮到與JAVA程序更好兼容。

契約校驗可在方法執行前后進行，這是契約式設計中最為關鍵的概念。方法契約被VeriJava定義全面覆蓋。方法本身可被覆寫或被重載，且擁有的標識符也不同，對此應對繼承類結構進行考慮。以布爾表達式的形式，將契約表達式放置于方法體和方法簽名之間。如果沒有將子句編寫上，那么后置條件與前置條件為true。方法契約并非適合所有方法，特別是PROTRCTED和PUBLIC方法會對其展開應用。因為PRIVATE方法是PROTECTED和PUBLIC方法的輔助實現，對外不可見，所以外界不會因此產生交互。

三、VERIJAVA 工具包

以ECLIPSE插件技術為基礎的開放式工具集合就是VeriJava工具包。工具包實現功能諸多，包括動態檢查器、編輯器、視圖、NATURE、向導等。VeriJava源文件及工程可通過VeriJava工具包來創建。VeriJava源文件的擴展名為vj，而命名規則相同于JAVA文件。因為BUILD擴展名已經在工具包中實現，因此在保存過程中，就會對VeriJava的編譯器調用。ECLIPSE擴展點可實現新功能的添加。例如：想將新的一項內容加入菜單，可利用ECLIPSE擴點實現。該擴展點一旦實現，同時就建立一個擴展，不僅如此，該擴展還能創新建立屬于自己的擴展點，由此得知，遞歸性是這種插件模式所特有的。通過不同擴展點，也能夠不斷實現VeriJava語言系統功能。工程類別屬性的唯一標識就是NATURE，在.PROJECT文件中能夠找到。在擁有多個NATURE屬性的工程中導入與NATURE條件相符的工具或試圖，且以vjnatrer為VeriJava的NATRER，在工程中導入VeriJava插件時，會對vjnatuer是否存在于該工程中進行檢查，如果不存在，則無法使用VeriJava工具。

四、結束語

契約式設計是一種設計計算機軟件的方法，將契約式設計引入程序中后，該設計的引入大幅增強了軟件系統完備性和充實性，以契約式設計為基礎實現異常情況的有效、安全處理；使人更好了解及操控繼承機制。在限定程序行為的同時，VeriJava語言中的方法契約自身不會將程序的狀態改變。方法契約被VeriJava定義全面覆蓋。方法本身可被覆寫或被重載，且擁有的標識符也不同，對此應對繼承類結構進行考慮。以布爾表達式的形式，將契約表達式放置于方法體和方法簽名之間。對VeriJava工具包的不斷優化及完善有助于深入分析。通過工具包的建立，為研究VeriJava程序提供支持。應用該工具便于VeriJava程序的創建及編寫。與此同時，VeriJava工具包還整合了插件，如動態檢查工具，軟件研發人員可直接動態驗證程序。隨著不斷深入的契約編程研究，如描述面向對象的UML中引入契約式設計等，不斷迎接新的挑戰。

參考文獻：

[1]朱鵬程，管致錦，衛麗華.可逆編程語言R-JAVA及其語言處理系統的設計[J].計算機工程與設計，2013（10）.

[2]焦繼業，穆榮，郝躍.快速設計高性能有符號乘法器電路的編程語言研究[J].電子學報，2013（11）.

[3]黃奉孝，高艷華，張學軍.基于嵌入式構件的編程語言融合技術研究[J].計算機工程與設計，2012（11）.