张 进，何成万，石 尤

武汉工程大学计算机科学与工程学院，湖北 武汉430205

契约式设计（design by contract，DbC），又叫合同设计方法，可以用于确保程序的准确性和提高程序的可靠性，它是基于Hoare的公理化证明方法而开发的设计思想［1］。基于合同的开发主要是通过在程序模块中添加前提条件、后置条件和不变量来为模块设计契约［2］。前提条件描述一个模块对调用该模块人员提出的要求，调用此模块之前必须满足该模块的前提条件。后置条件描述的是调用者在调用某模块之后应该满足的条件。不变量是对于整个模块而言，不变量必须在模块执行前后被满足。在面向对象的设计中使用合同编程的思想，形成了各种支持契约式的语言，如Eiffel、Larch、Java建 模 语 言（java modeling language，JML）、还有Microsoft.Net平台上的SPEC#等。其中，埃菲尔语言是最著名的规范语言［3］。

面向方面编程（aspect-oriented programming，AOP）通过封装横切关注点的思想为解决合同编程中所出现的代码交织等问题提供了很好的解决方案，并且，AOP的语言结构与契约之间也有着自然的对应关系［4］，当不变式以及前置条件和后置条件均看成横切关注点，AOP就可以很容易地完成它们与其他功能模块之间的相互分离，使得开发人员可以在独立的编织器模块中实现和编写这些模块的功能，并以较为灵活的方式调用它们［5］。AOP的这些特性正好可以弥补合同编程的缺陷，所以，在面向对象设计中使用AOP技术来支持合同设计是一个增强软件系统可靠性的新方法［6-7］。

但是，作为一种形式化的方法，基于AOP的契约很难执行。……