０引言

伴隨著軟件行業(yè)的飛速發(fā)展，軟件項目越來越龐大，其開發(fā)團隊需要越來越多的人參與其中。軟件行業(yè)人員的高度流動性以及國內(nèi)軟件項目管理的混亂，造成了代碼和文檔的不一致，使得程序的可重用性、可維護性比較差，軟件維護費用開銷太大。在這種情況下急需設(shè)計出一些好的程序分析工具進行程序剖析，例如自動給源程序生成注釋或規(guī)格說明來幫助人們理解程序，并保持基線管理的一致性［１］。合約式設(shè)計的思想根植于正規(guī)的（也就是數(shù)學(xué)形式的）軟件構(gòu)造分析方法。合約是由斷言所組成的，這些條件被用來描述前置條件、后置條件和不變量。一般情況下，軟件系統(tǒng)有４種合約類型。它們分別是語法合約、數(shù)據(jù)行為合約、控制合約和服務(wù)質(zhì)量合約。語法合約是控制性合約，而與語法合約不同的是，其他３種高層合約都不是強制性的，即使沒有數(shù)據(jù)行為合約、控制行為合約或服務(wù)質(zhì)量合約，軟件系統(tǒng)也能夠運行。但是不能保證良性運行。為了避免程序漏洞帶來的危害，提高程序的質(zhì)量，人們已進行了許多研究［２］。其中，基于合約的程序設(shè)計［３］（ＤｅｓｉｇｎＢｙＣｏｎｔｒａｃｔ，ＤＢＣ）就是一種十分重要且得到廣泛應(yīng)用的技術(shù)。從而，基于合約的程序動態(tài)分析也成為軟件質(zhì)量保證的一個重要途徑。

１合約的概念

從程序員的角度上講，程序就是為了解決某一實際問題的，用某種語言表示的一個有限指令序列；從邏輯的角度上理解，具體的一種計算機語言，就是符號邏輯中的一階語言，計算機語言中的語法規(guī)則就是一階語言中Ｌｔ的具體體現(xiàn)；語句就是一階語言中的公式，程序就是定義于此一階語言的一個結(jié)構(gòu)［４］。規(guī)范是軟件所需要滿足的需求和目的的體現(xiàn)，它是一種易于理解的精確而形式的陳述。以便恰當(dāng)?shù)伢w現(xiàn)需求。規(guī)范由２部分組成，第一，性質(zhì)規(guī)范是屬性的形式陳述。一般屬性涉及安全性、可靠性、健全性和有效性，它定義了程序?qū)λ锌赡艿膱?zhí)行必須具備的特征。第二，功能規(guī)范是功能需求的形式陳述。功能需求描述程序的需求行為。一般地，程序規(guī)范描述程序要達到“什么”，而不描述“如何”達到。也就是說規(guī)范以結(jié)果的形式描述行為。合約實際上就是一個程序必須滿足的規(guī)范，主要是由斷言組成的一個程序行為的約束集合，并對這些約束條件進行核查。簡化的講，合約就是“規(guī)范和核查”。所謂斷言［３］就是必須為真的假設(shè)，只有這些假設(shè)為真，程序才能做到正確無誤，從而確保高質(zhì)量軟件系統(tǒng)的出現(xiàn)。合約式設(shè)計的主要斷言包括前置條件（Ｐｒｅ－ｃｏｎｄｉ－ｔｉｏｎ）、后置條件（Ｐｏｓｔ－ｃｏｎｄｉｔｉｏｎ）和程序不變量（Ｉｎｖａｒｉ－ａｎｔ）［２－４］。前置條件（Ｐｒｅ－ｃｏｎｄｉｔｉｏｎ）是針對面向?qū)ο蟪绦蛟O(shè)計的方法，它規(guī)定了在調(diào)用該方法之前必須為真的條件。后置條件（Ｐｏｓｔ－ｃｏｎｄｉｔｉｏｎ）主要是針對方法而言的，它規(guī)定了方法順利執(zhí)行完畢之后必須滿足的條件。程序不變量（ＰｒｏｇｒａｍＩｎｖａｒｉａｎｔ）也可以叫作程序不變式，是指在程序的某個位置（例如Ｊａｖａ的類中某方法的入口點或出口點）可見的，所有變元之間用公式的形式描繪出來的關(guān)系（包括變元本身的變化情況）。它是針對整個類而言的，規(guī)定了該類任何實例用任何方法時都必須為真的條件。舉個簡單的例子：對某個類的方法ｍ入口點的分析得出結(jié)論：ｘ＝２＊ｙ＋３＊ｚ，也就是說不管使用什么樣的測試程序?qū)嵗@個類，變元ｘ，ｙ，ｚ在方法ｍ的入口點，始終滿足ｘ＝２＊ｙ＋３＊ｚ。那么，表達式ｘ＝２＊ｙ＋３＊ｚ對于該類來講就是一個程序不變量［５］。

２合約式程序設(shè)計

合約式設(shè)計（ＤｅｓｉｇｎＢｙＣｏｎｔｒａｃｔ，ＤＢＣ）的思想是由合約式設(shè)計之父ＢｅｒｔｒａｎｄＭｅｙｅｒ提出的。合約式設(shè)計本意是比較簡單的，就是在設(shè)計和編碼階段向面向?qū)ο蟪绦蛑屑尤霐嘌浴嘌詰?yīng)使用某種編程語言嵌入到程序中（而不是僅僅通過文檔加以聲明），只有這樣對于程序員來講才有意義，更好地支持測試和調(diào)試工作［４］。合約式設(shè)計，為編程者或者測試者提供了一個不同于傳統(tǒng)模式的觀測程序的視角維度，并且是一個特別重要的維度。但是，不是說原來的設(shè)計維度不要了，而是提醒設(shè)計者，還存在一個維度即合約的維度。合約式設(shè)計的思想與當(dāng)前主流設(shè)計思想是相輔相成的。合約式設(shè)計對于軟件開發(fā)來講意義是重大的，主要體現(xiàn)在下面３個方面。

２．１合約式設(shè)計有助于提高軟件質(zhì)量

合約式設(shè)計對編程過程中出現(xiàn)的“錯誤”進行了明確的處理，這種清晰的思路，對于提高產(chǎn)品的可靠性和正確性，作用是巨大的。合約本身是對于程序前提和功能的一種規(guī)范，而在編寫這些規(guī)范的時候，程序員看待程序的角度是不一樣的。特別是當(dāng)軟件規(guī)模達到一定程度，復(fù)雜到一定程度的時候，已經(jīng)沒有任何方法來確保軟件完全正確。但是如果開發(fā)者能夠以一個不同的角度來審視自己的程序，那么相當(dāng)于用兩道不同的工序來確保產(chǎn)品質(zhì)量，可靠性大幅度提高。

２．２合約式設(shè)計有助于得到優(yōu)秀的設(shè)計

在合約式設(shè)計的過程中，可以很清晰地劃分軟件模塊的權(quán)利和義務(wù)，這個劃分過程本身對于系統(tǒng)整體設(shè)計的幫助是特別大的。從而進一步可以對軟件模塊接口的設(shè)計及理解更加透徹，所以能夠使程序更加趨于完美。

２．３合約式設(shè)計有助于提高文檔與代碼的協(xié)同性

作為一個程序設(shè)計者，面臨的主要矛盾是要創(chuàng)造出“好”的設(shè)計。一個設(shè)計只有滿足簡單、清晰、強壯、靈活、高效才能算是“好”的設(shè)計。所謂簡單，就是避免無謂的復(fù)雜化；清晰，就是要讓設(shè)計緊湊明確，容易理解；強壯，就是設(shè)計質(zhì)量要高，錯誤少，易實現(xiàn)，便于測試；靈活，就是讓設(shè)計方案保持彈性，隨時變化，應(yīng)對需求變更；高效，就是要避免無謂的效率損失，盡可能提高系統(tǒng)性能。上述幾點，合約式設(shè)計都能滿足，從而使文檔與代碼的協(xié)同性得到充分提高［６］。

３基于合約的程序動態(tài)分析