基于契約式設(shè)計(jì)的VeriJava編程語(yǔ)言設(shè)計(jì).pdf

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

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

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