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

1、上海交通大學碩士學位論文基于契約式設計的VeriJava編程語言設計姓名：張思博申請學位級別：碩士專業(yè)：計算機軟件與理論指導教師：饒若楠趙建軍20070101上海交通大學基于契約式設計的VeriJava編程語言設計II為了能夠令Java在語言級別支持契約式設計，從而真正使契約的編寫與程序的開發(fā)同步，實現(xiàn)基于契約編程的開發(fā)模式。我們嘗試對Java語言進行擴展，在保留Java編程語言原有特性的基礎之上，為其在語言級別支持契約式設計。我們構建

2、出一種新的語言系統(tǒng)——VeriJava。本文利用BNF范式對VeriJava語言系統(tǒng)的詞法和語法進行了定義，并以此定義為基礎制定了規(guī)約說明。本課題實現(xiàn)了契約式設計中3個方面的契約條件，包括方法契約，類契約和非空類型。這些契約條件又可以按照校驗時機的不同分為靜態(tài)編譯期契約和動態(tài)執(zhí)行期契約。由于面向對象語言的多態(tài)和繼承等特殊性，我們對擴展之后語言系統(tǒng)中程序的行為進行了研究和分析，論述了幾種契約條件對面向對象程序可能出現(xiàn)的影響。為了實現(xiàn)程序的

3、可驗證性，本課題提出了一種基于AOP和Annotation的動態(tài)檢查方案，并在工具中予以實現(xiàn)。在實踐工作方面，我們構建了一套基于Eclipse插件的VeriJava開發(fā)工具包，允許開發(fā)者利用該開發(fā)工具創(chuàng)建基于VeriJava的程序。并將動態(tài)檢查工具良好的集成入VeriJava插件工具包之中，可以對程序進行執(zhí)行期的動態(tài)檢查。本文首先將介紹契約式設計的背景和發(fā)展，分析已有技術的優(yōu)劣，在此基礎上，給出VeriJava語言的語法與語義定義，然后