基于合约的程序分析

０引言

伴随着软件行业的飞速发展，软件项目越来越庞大，其开发团队需要越来越多的人参与其中。软件行业人员的高度流动性以及国内软件项目管理的混乱，造成了代码和文档的不一致，使得程序的可重用性、可维护性比较差，软件维护费用开销太大。在这种情况下急需设计出一些好的程序分析工具进行程序剖析，例如自动给源程序生成注释或规格说明来帮助人们理解程序，并保持基线管理的一致性［１］。合约式设计的思想根植于正规的（也就是数学形式的）软件构造分析方法。合约是由断言所组成的，这些条件被用来描述前置条件、后置条件和不变量。一般情况下，软件系统有４种合约类型。它们分别是语法合约、数据行为合约、控制合约和服务质量合约。语法合约是控制性合约，而与语法合约不同的是，其他３种高层合约都不是强制性的，即使没有数据行为合约、控制行为合约或服务质量合约，软件系统也能够运行。但是不能保证良性运行。为了避免程序漏洞带来的危害，提高程序的质量，人们已进行了许多研究［２］。其中，基于合约的程序设计［３］（ＤｅｓｉｇｎＢｙＣｏｎｔｒａｃｔ，ＤＢＣ）就是一种十分重要且得到广泛应用的技术。从而，基于合约的程序动态分析也成为软件质量保证的一个重要途径。

１合约的概念

从程序员的角度上讲，程序就是为了解决某一实际问题的，用某种语言表示的一个有限指令序列；从逻辑的角度上理解，具体的一种计算机语言，就是符号逻辑中的一阶语言，计算机语言中的语法规则就是一阶语言中Ｌｔ的具体体现；语句就是一阶语言中的公式，程序就是定义于此一阶语言的一个结构［４］。规范是软件所需要满足的需求和目的的体现，它是一种易于理解的精确而形式的陈述。以便恰当地体现需求。规范由２部分组成，第一，性质规范是属性的形式陈述。一般属性涉及安全性、可靠性、健全性和有效性，它定义了程序对所有可能的执行必须具备的特征。第二，功能规范是功能需求的形式陈述。功能需求描述程序的需求行为。一般地，程序规范描述程序要达到“什么”，而不描述“如何”达到。也就是说规范以结果的形式描述行为。合约实际上就是一个程序必须满足的规范，主要是由断言组成的一个程序行为的约束集合，并对这些约束条件进行核查。简化的讲，合约就是“规范和核查”。所谓断言［３］就是必须为真的假设，只有这些假设为真，程序才能做到正确无误，从而确保高质量软件系统的出现。合约式设计的主要断言包括前置条件（Ｐｒｅ－ｃｏｎｄｉ－ｔｉｏｎ）、后置条件（Ｐｏｓｔ－ｃｏｎｄｉｔｉｏｎ）和程序不变量（Ｉｎｖａｒｉ－ａｎｔ）［２－４］。前置条件（Ｐｒｅ－ｃｏｎｄｉｔｉｏｎ）是针对面向对象程序设计的方法，它规定了在调用该方法之前必须为真的条件。后置条件（Ｐｏｓｔ－ｃｏｎｄｉｔｉｏｎ）主要是针对方法而言的，它规定了方法顺利执行完毕之后必须满足的条件。程序不变量（ＰｒｏｇｒａｍＩｎｖａｒｉａｎｔ）也可以叫作程序不变式，是指在程序的某个位置（例如Ｊａｖａ的类中某方法的入口点或出口点）可见的，所有变元之间用公式的形式描绘出来的关系（包括变元本身的变化情况）。它是针对整个类而言的，规定了该类任何实例用任何方法时都必须为真的条件。举个简单的例子：对某个类的方法ｍ入口点的分析得出结论：ｘ＝２＊ｙ＋３＊ｚ，也就是说不管使用什么样的测试程序实例化这个类，变元ｘ，ｙ，ｚ在方法ｍ的入口点，始终满足ｘ＝２＊ｙ＋３＊ｚ。那么，表达式ｘ＝２＊ｙ＋３＊ｚ对于该类来讲就是一个程序不变量［５］。

２合约式程序设计

合约式设计（ＤｅｓｉｇｎＢｙＣｏｎｔｒａｃｔ，ＤＢＣ）的思想是由合约式设计之父ＢｅｒｔｒａｎｄＭｅｙｅｒ提出的。合约式设计本意是比较简单的，就是在设计和编码阶段向面向对象程序中加入断言。断言应使用某种编程语言嵌入到程序中（而不是仅仅通过文档加以声明），只有这样对于程序员来讲才有意义，更好地支持测试和调试工作［４］。合约式设计，为编程者或者测试者提供了一个不同于传统模式的观测程序的视角维度，并且是一个特别重要的维度。但是，不是说原来的设计维度不要了，而是提醒设计者，还存在一个维度即合约的维度。合约式设计的思想与当前主流设计思想是相辅相成的。合约式设计对于软件开发来讲意义是重大的，主要体现在下面３个方面。

２．１合约式设计有助于提高软件质量

合约式设计对编程过程中出现的“错误”进行了明确的处理，这种清晰的思路，对于提高产品的可靠性和正确性，作用是巨大的。合约本身是对于程序前提和功能的一种规范，而在编写这些规范的时候，程序员看待程序的角度是不一样的。特别是当软件规模达到一定程度，复杂到一定程度的时候，已经没有任何方法来确保软件完全正确。但是如果开发者能够以一个不同的角度来审视自己的程序，那么相当于用两道不同的工序来确保产品质量，可靠性大幅度提高。

２．２合约式设计有助于得到优秀的设计

在合约式设计的过程中，可以很清晰地划分软件模块的权利和义务，这个划分过程本身对于系统整体设计的帮助是特别大的。从而进一步可以对软件模块接口的设计及理解更加透彻，所以能够使程序更加趋于完美。

２．３合约式设计有助于提高文档与代码的协同性

作为一个程序设计者，面临的主要矛盾是要创造出“好”的设计。一个设计只有满足简单、清晰、强壮、灵活、高效才能算是“好”的设计。所谓简单，就是避免无谓的复杂化；清晰，就是要让设计紧凑明确，容易理解；强壮，就是设计质量要高，错误少，易实现，便于测试；灵活，就是让设计方案保持弹性，随时变化，应对需求变更；高效，就是要避免无谓的效率损失，尽可能提高系统性能。上述几点，合约式设计都能满足，从而使文档与代码的协同性得到充分提高［６］。

３基于合约的程序动态分析