本頁使用了標題或全文手工轉換

契約式設計

維基百科,自由的百科全書
跳至導覽 跳至搜尋
契約式設計模式

契約式設計(英語:Design by Contract,縮寫為 DbC),一種設計電腦軟體的方法。這種方法要求軟體設計者為軟體組件定義正式的,精確的並且可驗證的介面,這樣,為傳統的抽象資料類型又增加了先驗條件、後驗條件和不變式。這種方法的名字裡用到的「契約」或者說「契約」是一種比喻,因為它和商業契約的情況有點類似。

因為「Design by Contract」是屬於Eiffel Software的註冊商標,很多開發人員用契約式編程(Programming by Contract),契約編程(Contract Programming),或者契約優先式開發(Contract-First development)來指代這種方法。微軟也採用這種設計方法,稱為程式碼合約(Code Contracts)。

歷史[編輯]

這個術語最早由伯特蘭·邁耶於1986年提出。他設計了Eiffel程式語言來實現這種程式設計方法,在《物件導向軟體建構》(Object-Oriented Software Construction)一書中,又提出兩個後繼版本。2003年,由伯特蘭·邁耶建立的Eiffel software公司,申請將Design by Contract作為商標,於2004年通過。

契約式設計應用了形式驗證、Formal specification與霍爾邏輯的理論。

描述[編輯]

DbC的核心思想是對軟體系統中的元素之間相互合作以及「責任」與「權利」的比喻。這種比喻從商業活動中「客戶」與「供應商」達成「契約」而得來。例如:

  • 供應商必須提供某種產品(責任),並且他有權期望客戶已經付款(權利)。
  • 客戶必須付款(責任),並且有權得到產品(權利)。
  • 契約雙方必須履行那些對所有契約都有效的責任,如法律和規定等。

同樣的,如果在物件導向程式設計中一個的函式提供了某種功能,那麼它要:

  • 期望所有呼叫它的客戶模組都保證一定的進入條件:這就是函式的先驗條件—客戶的義務和供應商的權利,這樣它就不用去處理不滿足先驗條件的情況。
  • 保證退出時給出特定的屬性:這就是函式的後驗條件英語Postcondition—供應商的義務,顯然也是客戶的權利。
  • 在進入時假定,並在退出時保持一些特定的屬性:不變條件

契約就是這些權利和義務的正式形式。我們可以用「三個問題」來總結DbC,並且作為設計者要經常問:

  • 它期望的是什麼?
  • 它要保證的是什麼?
  • 它要保持的是什麼?

很多程式語言都有對這種斷言的支援。然而DbC認為這些契約對於軟體的正確性至關重要,它們應當是設計過程的一部分。實際上,DbC提倡首先寫斷言。

契約的概念擴充到了方法/過程的級別。對於一個方法的契約通常包含下面這些資訊:

繼承中的子類型可以弱化先驗條件(但不可以加強它們),並且可以加強後驗條件和不變式(但不能弱化它們)。這些原則很接近Liskov代換原則

所有類之間的關係就是客戶與供應商的關係。一個客戶在呼叫供應商的功能時有義務不去違反供應商所需的狀態。相應的,供應商也有義務為客戶提供它所需的狀態和資料。例如,供應商的delete功能要求客戶在data buffer當中有資料存在。相應的,供應商要保證當delete功能完成後,data buffer中的資料已被刪除。其它的設計契約還有不變式。不變式保證類的狀態在任何功能被執行後都保持在一個可接受的狀態。

當使用契約時,供應商不應對契約條件是否被滿足進行校驗。大體的思想是,利用契約條件校驗為保護網,在契約被違反的情況下代碼要「死翹翹」(fail hard)。DbC的「死翹翹」概念讓對契約行為的除錯變簡單,因為每個過程的行為意圖被定義得很清楚。它和一種叫作防禦性編程的方法明顯不同,在那種方法裡,供應商要負責解決先驗條件不滿足的情況。相對通常的情況下,在DbC和defensive programming中,如果客戶違反了先驗條件供應商都會丟擲異常—由客戶來負責解決這種情況。DbC讓供應商的工作更簡單。

DbC同時也定義了軟體模組的正確性條件:

  • 如果對一個供應商的呼叫之前類的不變式和先驗條件是真,那麼在呼叫後不變式和後驗條件也為真。
  • 當呼叫供應商時,軟體模組應保證不違反供應商的先驗條件。

因為契約條件在程式執行中不應被違反,它們可以只作為除錯代碼,或者在發布版本中被移除從而得到更好的效能。

DbC也能幫助代碼重用,因為每段代碼的契約都被很好的文件化了。模組的契約可以被當做軟體文件來 描述模組的行為。

語言支援[編輯]

原生支援語言[編輯]

貫徹契約式設計特徵最多的語言套件含:

通過第三方支援的語言[編輯]

參考文獻[編輯]

  1. ^ Bright, Walter. D Programming Language, Contract Programming. Digital Mars. 2006-08-20 [2006-10-06]. 
  2. ^ Findler, Felleisen Contracts for Higher-Order Functions