０引言

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

１合約的概念

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

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

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

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

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

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

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

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

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

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