前言：尋找寫作靈感？中文期刊網用心挑選的基于合約的程序分析，希望能為您的閱讀和創作帶來靈感，歡迎大家閱讀并分享。

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世紀計算機行業的一項重大突破。