上海交通大学硕士学位论文

基于契约式设计的Java编译器实现

学校：上海交通大学

院系：软件学院

专业：计算机软件与理论

班级：B0403791

学号：1040379006

作者姓名：张嘉铭

指导教师：赵建军

上海交通大学

2006年12月

基于契约式设计(DesignByContract,DBC)这一理论是由

BetrandMeyer提出的。DBC技术的核心是利用断言使方法及类的行

为受到契约的约束,因此,将DBC与高级语言相结合的方式成为DBC

技术的发展趋势。将DBC技术与现有的高级语言相结合的现有已实

现技术中,或多或少的存在着不足之处。同时,DBC与高级语言相

结合的方式不尽相同也带来了对于环境的不同的要求,在结合方式上

进行转变,为DBC与高级语言的结合寻觅新的途径已成为迫切的需

要。

VeriJava是由标准Java语言结合契约式设计方式而产生的新语

言,这一语言将契约作为语言要素添加入Java语言中,对方法进行

编译和运行时的检验,同时也通过类契约,不变量等契约要素,帮助

开发人员在开发的过程中及时找到设计错误或协调沟通问题,促进交

流与理解,检验与修正开发过程中所出现的各类设计错误等,使开发

过程更为完善。

本文通过实现一个基于VeriJava语法与语义检查,验证的编译器,

试图通过对方法的先决条件,后置条件以及对类契约,不变量等契约

要素的转换进行编译时与运行时验证,在逻辑上保证方法的正确性,契约式设计;Java;编译器DesignbyContract(DBC)ismentionedbyBetrandMeyer.Thekey

technologyofDBCistousethe“assertion”torestrictwhatthemethod

doesorwhatthewholeclassdoes,sothecombinationofDBCand

programminglanguagebecomesthetrendoftheDBCdevelopment.The

combinationtechnologyexistednowhavesomedisadvantagesandthe

differenceofwaysofcombinationbringupthedifficultyofenvironment

requirement.Seekingfornewcombinationmethodcomestobethe

urgentrequirement.

VeriJavaisanewprogramminglanguagewhichiscombinedofDBC

andstandardJavalanguage,itaddsnotonlythecontractasatotally

languagefactorintotheJavalanguagetoverifythemethodduring

runtimeandcompiletime,andalsousecontractintheclassareatohelp

thedevelopertofindouttheproblemofdesignorthemisunderstanding

betweenprogrammers,itcanalsousetocorrectthemistakesmadeduring

designdecadeandcoding,forbettersoftwaredevelopment.

ThispaperrealizeacompilerofVeriJavagra