程序的正确性是软件开发中的核心问题，也是软件质量的基础，为了能够解决该问题，开发出无错的软件，人们提出了许多方法。形式化方法是其中的一种，它试图用严格的数学理论来规范和指导程序设计，从而保证软件的正确性。但是，形式化方法有着严格的数学理论，对开发者的要求比较高，因而，在实践中的应用并不是非常普遍。契约式开发方法(Design By Contract，DBC)[1]是一种借鉴了形式化方法优点而又易于实践的开发方法学，它引入了形式化方法中的不变式、前置谓词和后置谓词等概念，来精确刻画程序模块的语义。契约式方法提供了方便的定义规约和检查规约的手段，使得开发者在实际开发过程中能够真正利用形式化方法的优点。在面向对象开发领域中，契约式开发已经是一种被普遍接受的用于提高软件可靠性的系统化方法。但是，契约式开发也有其不利的方面，比如编写程序时的“额外负担”、不同关注点的代码纠缠等等，因此，主流的面向对象语言并未提供对它的支持。面向方面编程[2](Aspect-Oriented Programming，AOP)是一种新兴的编程技术，近年来已逐渐成为程序设计领域的热点。它强调关注点的分离和横切关注点的封装，被人们认为是解决面向对象系统固有问题的“灵丹妙药”。AOP的语言构造与契约式开发之间存在着天然的对应关系，这一特点恰好可以弥补契约式开发方法的不利方面，因此，利用AOP技术在面向对象系统中支持契约式开发是提高软件系统可靠性的途径。目前存在的将AOP实现应用于契约式开发的方法主要分为两类：一类是使用AOP的具体实现语言(如AspectJ)来支持主流的面向对象语言的契约式开发。在这种情况下，与契约相关的代码从业务逻辑代码中彻底分离出来了，节省了大量重复的契约检查代码。但是，这类方法依赖于语言的具体实现细节，要求程序员掌握AOP实现语言的复杂语法，对程序员而言是一种挑战和负担；再则，这种方法只能用于实现阶段，而无法在设计阶段对契约进行精确的定义和描述。第二类方法则借助于相对比较成熟和完善的规范语言(如OCL)进行契约约束，然后通过一定的转换规则将其转换成AspectJ等AOP实现语言。这类方法可以在设计阶段精确地描述各种谓词和不变式条件，但是，鉴于大多数规范语言都是建立在形式语言的基础之上的，因此其表达式一般比较冗长，理解起来不直观；而且，因为OCL等规范语言和AspectJ等AOP实现语言在抽象程度上有着很大的差异，从而导致两者在转换的实现上存在着一定的困难。在本文中，作者分别深入研究了面向方面编程技术和契约式开发，发现了两者之间的联系，结合目前AOP在契约式开发中暴露出来的问题，提出了一种改善和提高基于AOP的契约式开发方法的方案。该方案集成了基于AOP的契约式软件开发流程的整个过程，填补了基于AOP的契约式开发中上层设计和下层实现之间的鸿沟，将两者融会贯通。本文首先给出了AOP和DBC之间的对应关系，在此基础上，提出了一种基于AOP的契约描述语言(ACDL)，该语言以AOP的方式表示契约，可以在设计阶段就精确而直观地描述类不变式、方法的前置、后置条件，而不依赖于任何AO的语言细节；另一方面，由于其在语言的表达风格上接近于AO，因此，可以很容易地向AspectJ等AOP实现语言转换。同时，本文对ACDL语言与上层设计和下层实现之间的联系进行了阐述，分析了他们之间转换的可行性，并探讨了ACDL语言在实际软件开发过程中的作用和意义。最后，本文给出了ACDL语言辅助工具AJMaker的实现框架，该工具可以根据用户给出的不变式和谓词信息自动生成ACDL代码，也可将ACDL代码解析成AspectJ代码。