基本介紹
- 中文名：契約式設計
- 外文名：Design by Contract
- 簡稱：DbC
- 定義：一種設計計算機軟體的方法
定義,描述,對面向對象的幾點衝擊,契約式設計的三個關鍵字,DbC六大原則,契約式設計與斷言,
定義
所謂契約，也就是契約，規定兩個互動物件上的權利和責任。
僱傭契約規定你的工作時數和你必須遵守的行為規則，作為公司則付你薪水，雙雙履行義務，雙雙受益。
在應用程式中，Eiffel語言首先提供了《按契約設計》的概念，它關注的是用程式規定軟體模組的權利和責任，以確保程式正確性。用文檔記載權利和義務的說明，用程式來校驗，這就是《契約式設計》的核心。Design by Contract（DbC，契約式設計）是面向對象軟體大師Bertrand Meyer對軟體構造方法的一個重大貢獻，無論是在形式化的數學證明中，還是在實踐運用中，都被證明是大幅改善軟體工程質量的有效手段。該方法在Eiffel程式語言中獲得直接支持，並且可以通過輔助工具在Java語言中運用。
因為Design by Contract是一個屬於Eiffel Software的註冊商標，很多開發人員用“Programming by Contract”, “Contract Programming”, 或者”Contract-First development“來指代這種方法。
描述
DbC的核心思想是對軟體系統中的元素之間相互合作以及“責任”與“義務”的比喻。這種比喻從商業活動中“客戶”與“供應商”達成“契約”而得來。例如：
1.供應商必須提供某種產品（責任），並且他有權期望客戶已經付款（權利）。
2.客戶必須付款（責任），並且有權得到產品（權利）。
3.契約雙方必須履行那些對所有契約都有效的責任，如法律和規定等。
1.期望所有調用它的客戶模組都保證一定的進入條件：這就是函式的先驗條件—客戶的義務和供應商的權利，這樣它就不用去處理不滿足先驗條件的情況。
2.保證退出時給出特定的屬性：這就是函式的後驗條件—供應商的義務，顯然也是客戶的權利。
3.在進入時假定，並在退出時保持一些特定的屬性：不變式。
契約就是這些權利和義務的正式形式。我們可以用“三個問題”來總結DbC，並且作為設計者要經常問：
1.它期望的是什麼？
2.它要保證的是什麼？
3.它要保持的是什麼？
很多語言都有對這種斷言的支持。然而DbC認為這些契約對於軟體的正確性至關重要，它們應當是設計過程的一部分。實際上，DbC提倡首先寫斷言。
契約的概念擴展到了方法/過程的級別。對於一個方法的契約通常包含下面這些信息：
1.可接受和不可接受的值或類型，以及它們的含義
2.返回的值或類型，以及它們的含義
3.可能出現的錯誤以及異常情況的值和類型，以及它們的含義
4.副作用
5.先驗條件
6.後驗條件
7.不變式
8.(不太常見) 性能上的保證，如所用的時間和空間
繼承中的子類型可以弱化先驗條件（但不可以加強它們），並且可以加強後驗條件和不變式（但不能弱化它們）。這些原則很接進Liskov代換原則。
所有類之間的關係就是客戶與供應商的關係。一個客戶在調用供應商的功能時有義務不去違反供應商所需的狀態。相應的，供應商也有義務為客戶提供它所需的狀態和數據。例如，供應商的delete功能要求客戶在data buffer當中有數據存在。相應的，供應商要保證當delete功能完成後，data buffer中的數據已被刪除。其它的設計契約還有不變式。不變式保證類的狀態在任何功能被執行後都保持在一個可接受的狀態。
當使用契約時，供應商不應對契約條件是否被滿足進行校驗。大體的思想是，利用契約條件校驗為保護網，在契約被違反的情況下代碼要“死翹翹”（fail hard）。DbC的“死翹翹”概念讓對契約行為的調試變簡單，因為每個過程的行為意圖被定義得很清楚。它和一種叫作defensive programming的方法明現不同，在那種方法裡，供應商要負責解決先驗條件不滿足的情況。相對通常的情況下，在DbC和defensive programming中，如果客戶違反了先驗條件供應商都會拋出異常—由客戶來負責解決這種情況。DbC讓供應商的工作更簡單。
DbC同時也定義了軟體模組的正確性條件：
1.如果對一個供應商的調用之前類的不變式和先驗條件是真，那么在調用後不變式和後驗條件也為真。
2.當調用供應商時，軟體模組應保證不違反供應商的先驗條件。
因為契約條件在程式運行中不應被違反，它們可以只作為調試代碼，或者在發布版本中被移除從而得到更好的性能。
DbC也能幫助代碼重用，因為每段代碼的契約都被很好的文檔化了。模組的契約可以被當做軟體文檔來 描述模組的行為。
對面向對象的幾點衝擊
一 Server和Client的衝擊：
程式庫和組件庫被類比為server，而使用程式庫、組件庫的程式被視為client。根據這種C/S關係，我們往往對庫程式和組件的質量提出很嚴苛的要求，強迫它們承擔本不應該由它們來承擔的責任，引入契約觀念之後，這種C/S關係被打破，大家都是平等的，你需要我正確提供服務，那么你必須滿足我提出的條件，否則我沒有義務“排除萬難”地保證完成任務。
二 權利和義務的關係：
一般認為在模組中檢查錯誤狀況並且上報，是模組本身的義務。而在契約體制下，對於契約的檢查並非義務，實際上是在履行權利。一個義務，一個權利，差別極大。例如上面的代碼：
if (dest == NULL) { ... }
這就是義務，其要點在於，一旦條件不滿足，我方（義務方）必須負責以合適手法處理這尷尬局面，或者返回錯誤值，或者拋出異常。而：
assert(dest != NULL);
檢查契約，履行權利。如果條件不滿足，那么錯誤在對方而不在我
三 確保必須條件：
契約所核查的，是“為保證正確性所必須滿足的條件”，因此，當契約被破壞時，只表明一件事：軟體系統中有bug。其意義是說，某些條件在到達我這裡時，必須已經確保為“真”。
assert(dest != NULL);
報錯時，你要做的不是去修改你的string_copy函式，而是要讓任何代碼在調用string_copy時確保dest指針不為空
四 “函式”和“過程”的理解：
我們以往對待“過程”或“函式”的理解是：完成某個計算任務的過程，這一看法只強調了其目標，沒有強調其條件 。引入契約之後，“過程”和“函式”被定義為：完成契約的過程。基於契約的相互性，如果這個契約的失敗是因為其他模組未能履行契約 ，本過程只需報告，無需以任何其他方式做出反應。而真正的異常狀況是“對方完全滿足了契約，而我依然未能如約完成任務”的情形。這樣以來，我們就給“異常”下了一個清晰、可行的定義。
契約式設計的三個關鍵字
一 前置條件（precondition）：
為了調用函式，必須為真的條件，在其違反時，函式決不調用，傳遞好數據是調用者的責任。
二 後置條件 （postcondition）：
函式保證能做到的事情，函式完成時的狀態，函式有這一事實表示它會結束，不會無休止的循環
三 類不變項（class invariant）：
從調用者的角度來看，該條件總是為真，在函式的內部處理過程中，不變項可以為變，但在函式結束後，控制返回調用者時，不變項必須為真。
DbC六大原則
原則1 區分命令和查詢。查詢返回一個結果，但不改變對象的可見性質。命令改變對象的狀態，但不返回結果。（應當是不一定返回結果）
原則 2 將基本查詢同派生查詢分開。派生查詢可以用基本查詢來定義。
原則 3 針對每個派生查詢，設定一個後驗條件，使用一個或多個基本查詢的結果來定義它。這樣我們只要知道基本查詢的值，也就能知道派生查詢的值。
原則 4 對於每個命令都撰寫一個後驗條件，規定每個基本查詢的值。結合“用基本查詢定義派生查詢”的原則，我們現在已經能夠知道每個命令的全部可視效果。
原則 5 對於每個查詢和命令，採用一個合適的先驗條件。先驗條件限定了客戶調用查詢和命令的時機。
原則 6 撰寫不變式來定義對象的恆定特性。類是某種抽象的體現，應當將注意力集中在最重要的屬性上，以幫助讀者建立關於類抽象的正確概念模型。
契約式設計與斷言
斷言可以看做是契約式設計的一個縮影或者是一部分，因為你不可能做DBC所做的一切事情。
斷言不能沿著繼承層次往下遺傳。如果你重新定義 了某個具有契約的基類方法，實現該契約的的斷言不會被正確調用（除非你再新的代碼中複製他們），你必須手工調類不變項，基本的契約不會主動實現。
