０引言

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

１合約的概念

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

２合約式程序設計

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

２．１合約式設計有助于提高軟件質量

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

２．２合約式設計有助于得到優秀的設計

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

２．３合約式設計有助于提高文檔與代碼的協同性

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

３基于合約的程序動態分析