前言：寻找写作灵感？中文期刊网用心挑选的基于合约的程序分析，希望能为您的阅读和创作带来灵感，欢迎大家阅读并分享。
0引言 伴随着软件行业的飞速发展，软件项目越来越庞大，其开发团队需要越来越多的人参与其中。软件行业人员的高度流动性以及国内软件项目管理的混乱，造成了代码和文档的不一致，使得程序的可重用性、可维护性比较差，软件维护费用开销太大。在这种情况下急需设计出一些好的程序分析工具进行程序剖析，例如自动给源程序生成注释或规格说明来帮助人们理解程序，并保持基线管理的一致性［1］。合约式设计的思想根植于正规的（也就是数学形式的）软件构造分析方法。合约是由断言所组成的，这些条件被用来描述前置条件、后置条件和不变量。一般情况下，软件系统有4种合约类型。它们分别是语法合约、数据行为合约、控制合约和服务质量合约。语法合约是控制性合约，而与语法合约不同的是，其他3种高层合约都不是强制性的，即使没有数据行为合约、控制行为合约或服务质量合约，软件系统也能够运行。但是不能保证良性运行。为了避免程序漏洞带来的危害，提高程序的质量，人们已进行了许多研究［2］。其中，基于合约的程序设计［3］（DesignByContract，DBC）就是一种十分重要且得到广泛应用的技术。从而，基于合约的程序动态分析也成为软件质量保证的一个重要途径。 1合约的概念 从程序员的角度上讲，程序就是为了解决某一实际问题的，用某种语言表示的一个有限指令序列；从逻辑的角度上理解，具体的一种计算机语言，就是符号逻辑中的一阶语言，计算机语言中的语法规则就是一阶语言中Lt的具体体现；语句就是一阶语言中的公式，程序就是定义于此一阶语言的一个结构［4］。规范是软件所需要满足的需求和目的的体现，它是一种易于理解的精确而形式的陈述。以便恰当地体现需求。规范由2部分组成，第一，性质规范是属性的形式陈述。一般属性涉及安全性、可靠性、健全性和有效性，它定义了程序对所有可能的执行必须具备的特征。第二，功能规范是功能需求的形式陈述。功能需求描述程序的需求行为。一般地，程序规范描述程序要达到“什么”，而不描述“如何”达到。也就是说规范以结果的形式描述行为。合约实际上就是一个程序必须满足的规范，主要是由断言组成的一个程序行为的约束集合，并对这些约束条件进行核查。简化的讲，合约就是“规范和核查”。所谓断言［3］就是必须为真的假设，只有这些假设为真，程序才能做到正确无误，从而确保高质量软件系统的出现。合约式设计的主要断言包括前置条件（Pre－condi－tion）、后置条件（Post－condition）和程序不变量（Invari－ant）［2－4］。前置条件（Pre－condition）是针对面向对象程序设计的方法，它规定了在调用该方法之前必须为真的条件。后置条件（Post－condition）主要是针对方法而言的，它规定了方法顺利执行完毕之后必须满足的条件。程序不变量（ProgramInvariant）也可以叫作程序不变式，是指在程序的某个位置（例如Java的类中某方法的入口点或出口点）可见的，所有变元之间用公式的形式描绘出来的关系（包括变元本身的变化情况）。它是针对整个类而言的，规定了该类任何实例用任何方法时都必须为真的条件。举个简单的例子：对某个类的方法m入口点的分析得出结论：x＝2＊y＋3＊z，也就是说不管使用什么样的测试程序实例化这个类，变元x，y，z在方法m的入口点，始终满足x＝2＊y＋3＊z。那么，表达式x＝2＊y＋3＊z对于该类来讲就是一个程序不变量［5］。 2合约式程序设计 合约式设计（DesignByContract，DBC）的思想是由合约式设计之父BertrandMeyer提出的。合约式设计本意是比较简单的，就是在设计和编码阶段向面向对象程序中加入断言。断言应使用某种编程语言嵌入到程序中（而不是仅仅通过文档加以声明），只有这样对于程序员来讲才有意义，更好地支持测试和调试工作［4］。合约式设计，为编程者或者测试者提供了一个不同于传统模式的观测程序的视角维度，并且是一个特别重要的维度。但是，不是说原来的设计维度不要了，而是提醒设计者，还存在一个维度即合约的维度。合约式设计的思想与当前主流设计思想是相辅相成的。合约式设计对于软件开发来讲意义是重大的，主要体现在下面3个方面。 2．1合约式设计有助于提高软件质量 合约式设计对编程过程中出现的“错误”进行了明确的处理，这种清晰的思路，对于提高产品的可靠性和正确性，作用是巨大的。合约本身是对于程序前提和功能的一种规范，而在编写这些规范的时候，程序员看待程序的角度是不一样的。特别是当软件规模达到一定程度，复杂到一定程度的时候，已经没有任何方法来确保软件完全正确。但是如果开发者能够以一个不同的角度来审视自己的程序，那么相当于用两道不同的工序来确保产品质量，可靠性大幅度提高。 2．2合约式设计有助于得到优秀的设计 在合约式设计的过程中，可以很清晰地划分软件模块的权利和义务，这个划分过程本身对于系统整体设计的帮助是特别大的。从而进一步可以对软件模块接口的设计及理解更加透彻，所以能够使程序更加趋于完美。 2．3合约式设计有助于提高文档与代码的协同性 作为一个程序设计者，面临的主要矛盾是要创造出“好”的设计。一个设计只有满足简单、清晰、强壮、灵活、高效才能算是“好”的设计。所谓简单，就是避免无谓的复杂化；清晰，就是要让设计紧凑明确，容易理解；强壮，就是设计质量要高，错误少，易实现，便于测试；灵活，就是让设计方案保持弹性，随时变化，应对需求变更；高效，就是要避免无谓的效率损失，尽可能提高系统性能。上述几点，合约式设计都能满足，从而使文档与代码的协同性得到充分提高［6］。 3基于合约的程序动态分析#p#分页标题#e# 关于程序行为描述的生成方法已经有了大量的研究，这方面的工作主要可以分为2种类型———静态分析和动态分析。静态分析方法通过检查程序代码等文档，发现系统隐含的性质，从而产生相应的形式化规格说明，也就是合约。在一定的条件下静态分析方法确实能够发现程序中所隐含的重要性质，但是这类技术通常只能成功应用于小规模的程序。近来研究发现，通过程序的实际（重复）运行，发现其行为合约的动态分析方法才是更适合的方法。其实动态分析和静态分析是相辅相成的。一般情况下动态分析产生“程序不变量”，即通过几组数据集的执行获得某些属性是真的信息；静态分析可以帮助确定这些不变量是不是真的不变量。当静态分析与动态分析不一致时有2种情况，即动态检测过程错误，以及由于静态分析没有分析所有可能路径而得出偏激结果。 3．1静态分析 静态分析是检验确认软件系统的一种方法。它的主要特点是无需运行软件系统本身，而对需求分析、设计和编码阶段得到的文件进行检验，以保证软件质量。主要有3种检验方法：针对需求说明的静态分析、针对设计文件的静态分析、针对源程序的静态分析。其中对程序做静态分析有2种做法，即程序特性信息分析和程序正确性分析。 3．2动态分析 现在把程序动态分析技术分为2种方式： 3．2．1传统方式的程序动态分析 对被测程序进行动态分析是要在运行被测程序的条件下，取得程序的动态特性信息。传统的动态分析通常要经历的过程是：（1）针对需求说明书的程序动态分析。典型方法是功能测试（即黑盒测试）。（2）针对设计文件的程序动态分析。根据设计过程中所涉及到的计算公式、算法、模块功能及接口等设计环节，提出测试数据，进行动态测试［6］。（3）针对源程序的动态测试。根据程序结构，包括程序中的语句、分支、路径或根据数据流、表达式、设计测试数据所完成的动态测试，常用的是分支测试和路径测试［3］。 3．2．2合约式的程序动态分析 提到合约式的程序动态分析［4］，一般都会想到合约和合约式程序设计的概念。那么什么是合约式的程序动态分析呢，首先它是一种程序动态分析方法，其次这种方法运用了合约式程序设计的基本思想，它建立在传统程序动态分析技术基础之上。主要分为针对设计文件的合约式程序动态分析和针对源程序的合约式程序动态测试。这两者在实际过程中应该是结合在一起的。 无论是一般程序设计还是在合约式程序设计过程中，必然要对整体程序中的模块、接口、类、变量等进行详尽分析。那么，它们之间肯定满足某些特定关系，这些所谓的特定关系就是程序无论如何运行，无论采用什么样的测试用例运行都要满足。合约式的程序动态分析方法就是，通过向待测程序中插入断言，然后编译运行，从而达到检测这些所谓的特定关系是否真正满足的目的。确定问题的所在。下面介绍一下具体过程。进行合约式的程序动态分析对设计文件的动态分析是必不可少的，在这个基础上分析出了类与类之间、变量之间、接口与类之间等等应该满足的必要条件。这些属性是保证软件正常运行的必要条件，在函数的入口处或者在类的开始位置，以断言的方式把所有属性写入源程序中，形成一个和原来程序同名的程序，然后运行该程序，如果出现异常，那么可以精确定位到出错位置，否则认为软件是合格的。概要流程如图1所示。由图1中可以看出，要进行合约式程序动态分析的一个必要条件是需要一个支持合约的程序编译器，例如，现有的Eiffel，JML编译器等。 目前，基于合约的程序动态分析做的比较好的是麻省理工学院计算机和人工智能研究所，他们开发了以发掘程序动态不变量为主要任务的动态不变量检测工具Daikon。Daikon是美国MIT程序分析组自1998年开始研究的，用Java语言开发的不变量检测工具，用于分析程序数据结构、动态分析程序不变量［7］。Daikon的主要依据是基于合约的程序动态分析理论，对程序进行动态检测，从而达到精确发现不变量的目的。ISEInc的Eiffelsoftware是一款支持合约式程序设计的软件，它的内嵌编译器同样支持合约式的程序编译，那么程序动态分析可以借助于Eiffel的编译器进程程序的分析检测［6，8］。现在的主要任务是针对任何语言开发一款支持所有语言的合约式程序分析编译器，如果这样就可以对任何程序进行合约式程序动态分析。当然现在已经出现了针对个体语言的合约式编译器，例如针对Java语言的JML编译器、iContract编译器等［1，9］。 4结语 无论静态分析还是动态分析，它们最终目标都是为了保证软件质量。如果能开发出新一代的编程语言，它能够把合约式的编程理念融入到其中，使编程者把合约断言等都写入编程代码中，并支持合约式程序的动态分析，那么这势必是21世纪计算机行业的一项重大突破。