契約式設計(design by contract)把類和它的客戶程式之間的關係看作正式的協議，描述雙方的權利和義務。bertrand meyer把它稱作構建物件導向軟體系統方法的核心。
契約式設計的提出，主要基於軟體可靠性方面的考慮。可靠性包括正確性和健壯性，正確性指軟體按照需求規格執行的能力，健壯性指軟體對需求規格中未宣告狀況的處理能力。健壯性主要與異常處理機制相關 。正確性一方面包括物件元素內部執行的正確性，另乙個重要方面是與其它物件元素互動時的正確性。客戶程式(client) methoda呼叫提供者(provider) methodb時，先需要按照methodb的要求準備好引數，這是methoda的責任；然後methodb需要按照功能規格正確的進行處理，將結果返回給呼叫者methoda，這是methodb的責任，也是methoda應得的利益。契約的雙方都有自己的責任和利益，在
building bug-free o-o software: an introduction to design by contract ™中，bertrand meyer給出了示例，從實際生活中的契約引申到物件元素間的契約。契約式設計就是要求提供一套機制，在客戶程式與提供者之間明確的宣告雙方的職責與權利，即契約，並能夠對這些契約進行驗證。 在
object-oriented software construction中bertrand meyer提到，正確性是乙個相對概念，只有跟具體的需求規格聯絡在一起，才有正確與不正確之分。在契約式設計中，用斷言(assersion)來描述需求規格。 c、c++等語言中有assert指令，這些指令只是對物件導向方法中的斷言非常有限的一種運用。
building bug-free o-o software: an introduction to design by contract ™中的例子：向乙個有限容量的字典（使用字串鍵值訪問各個元素）中插入某個元素，契約如下：
義務
權利
客戶程式
(必須保證前置條件)
確保字典沒有滿，鍵值是非空字串
(從後置條件獲益)
更新字典使新的元素出現在字典中，並跟給定的鍵關聯起來
提供者
(必需保證後置條件)
將給定元素放入字典中，並跟給定的鍵關聯起來
(可以假定前置條件成立)
如果字典滿了，或者鍵值為空字串，可以不處理
使用eiffel語法描述：假如這是乙個范型類dictionary[element]的put方法
put(x:element;key:string)x .count < capacitykey.empty
... some insertion algorithm ...
has (x)
item (key)= x
count =count + 1
require語句包含的是前置條件(precondition)，ensure語句包含的是後置條件(postcondition)，這些都是斷言，也就是契約的描述。
前置條件：當前的元素個數count小於容量capacity；鍵值key不是空字串。
後置條件：字典中存在元素x；使用健值key獲取的元素是x；操作後元素個數count等於操作前元素個數old count加一(eiffel中有old關鍵字)。
在整個軟體過程中，從概念模型的business use case用例規約開始就會有很多前置、後置條件 ，這些條件被具體化到設計模型後，就是每個物件元素的契約了。
保證前置條件是客戶程式的職責，保證後置條件是服務提供者(被呼叫方法)的職責。
條件的強弱(strong and weak condition)：條件p1包含p2並且不等於p2，就說條件p1比p2強，p2比p1弱。
繼承關係中，子類如果重寫父類方法需要重定義斷言，原則是：前置條件應當與父類相同或比父類弱；後置條件應當與父類相同或比父類強。這樣在多型運用的地方可以確保：滿足父類的前置條件一定可以滿足子類，子類的後置條件一定會滿足父類的後置條件。
前置條件和後置條件運用在各個方法上，有的契約描述需要運用在整個類層次上，這種契約(斷言)叫做類不變數(class invariants)。例如dictionary的例子中，不變數可能是下面這樣：
invariant
0 <= count
andcount <= capacity 在
building bug-free o-o software: an introduction to design by contract ™中，bertrand meyer談到了契約式設計其它的一些好處：
1. 文件。在文件中不僅包含簽名描述，也能包含契約描述，如果能更進一步象visualstudio智慧型提示那樣呈現，能減少很多編碼過程中犯下錯誤。
2. 測試、除錯、品質保證。nunit是比較完善的斷言測試框架，如果語言本身提供契約式設計支援，我們可以使單元測試中斷言的覆蓋範圍更廣泛（考慮一般都是開發者自己做單元測試），能夠幫助發現更多隱性的缺陷，斷言測試**的編寫會更簡潔。
我們習慣性的在函式內部檢查各個前置條件是否符合要求，例如各個入參是否符合規定等(防禦式程式設計-defensive programming)，契約式設計反對這種做法。呼叫者可能會自己做檢查，保證這些前置條件符合要求，這樣這些條件可能被多次檢查；另外將這些條件檢查夾雜在邏輯**中實現，使得契約並不是明確的描述出來，也增加了實現**的複雜性。從微觀角度來看(即乙個個函式的角度)，這並沒有什麼害處，但從巨集觀的角度看，複雜性是品質問題的主要原因。契約式設計中將這些條件集中明確的宣告，確定職責歸屬，並由框架輔助進行驗證。
契約式設計要求客戶程式確保前置條件，在
object-oriented software construction中bertrand meyer把這種方式叫做強制型方式(demanding style)；相反地由服務提供者自己進行條件驗證的方式稱為寬容型方式(tolerant style)。他列舉了現實中的乙個例子，老職員對於不符合要求的申請，可能一概拒絕；而乙個職場新手可能採取的態度是嘗試自己為那些申請糾正錯誤、補充完整。
在接收外部輸入的地方，還是必須做校驗，應當使用專門的驗證模組實現。
c、c++中使用assert斷言以方便測試、除錯；nunit使用assert斷言框架進行測試；bertrand meyer開發eiffel語言，充分的展現語言層面對契約式設計的支援。如果這些斷言使用方式可以看作是自底向上的運用契約思想，那tdd就可以看作是自頂向下運用契約思想的方式，並且深入到用它驅動整個軟體過程。
codeproject上有乙個c#的契約式設計框架：
design by contract framework，實現很簡潔，因為語言層面沒有提供支援，它的實現方式基本上跟c、c++中的assert完全一樣。
良好的契約編寫能力是乙個難點，我們是通過布林型的斷言來描述規格(specification)，如何準確地表達是一門藝術。另外也跟分析設計粒度結合在相關，例如乙個類、方法，如果粒度過大所完成的任務過雜，準確地描述前置、後置條件、不變式可能就非常困難。
目前eiffel在語言層級支援契約式設計，但限於序列程式(sequential program)，對於並行領域中契約式設計的運用，更在探索中。
Design by Contract（契約式設計）
design by contract 是bertrand meyer 總結的一項設計技巧 design by contract 的核心是斷言 assertion 所謂 斷言 是指永遠為真的布林型語句，如果不為真，則程式必然存在錯誤。通常情況下，檢查斷言的時機，應該侷限於除錯 debug 階段，而不是...
Design by Contract（契約式設計）
dbc 元素 先驗條件 針對方法 method 它規定了在呼叫該方法之前必須為真的條件。後驗條件 也是針對方法，它規定了方法順利執行完畢之後必須為真的條件。不變式 針對整個類，它規定了該類任何例項呼叫任何方法都必須為真的條件。dbc 六大原則 區分命令和查詢 將基本查詢同派生查詢區分開 針對每個派生...
契約式程式設計
契約是減少大型專案成本的突破性技術。契約由先驗條件 後驗條件 錯誤和不變數等概念組成。契約可以而加到 c 中而無需對語言加以改造，但是卻十分笨拙且不一致。在語言內部支援契約的目的是 給契約乙個一致的觀感 提供工具支援 使編譯器能夠根據從契約中收集的資訊生成更好的 易於管理並強制實行契約 處理契約繼承...