论文摘要
基于契约进行程序验证的理论最早出现于20世纪70年代对大型系统的研究之中。20世纪90年代,Bertrand Meyer首次将契约式设计（Design by Contract, DbC）理念引入了面向对象编程技术中,并且在其构建的Eiffel语言中进行了全面的支持。现在,契约式设计已经发展成为构建高质量和可靠性软件的一种重要的软件工程方法,并且越来越受到学术界和工业界的关注。契约式设计通过在程序中引入前置条件,后置条件和常量等契约条件的方式,在应用程序的服务提供者与调用者之间建立了一种需要双方相互满足的契约关系。可以通过对契约条件进行动态检查或静态验证的方式来实现程序的可验证性。目前,已经有多种编程语言直接或间接地支持了契约式设计的理念,这其中包括C++和C#等被程序开发者广泛使用的高级面向对象语言。Java作为主流编程语言之一,自身并不支持契约式设计的理念。近年来虽然出现了一些将契约式设计引入Java语言中技术手段,但基本都是通过Java内部的某些机制或者改变Java虚拟机的行为来实现的。这类实现方式使契约的编写与程序分离,契约和编写校验不具有强制性,或者契约仅仅是程序的补丁。因此,都没有实现令Java编程语言自身完全支持契约式设计。而JDK1.4中引入的断言（assert）并不能完全涵盖契约式设计的全部特性。