Loading AI tools
来自维基百科,自由的百科全书
契約式設計(英語: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年通過。
DbC的核心思想是對軟體系統中的元素之間相互合作以及「責任」與「權利」的比喻。這種比喻從商業活動中「客戶」與「供應商」達成「契約」而得來。例如:
同樣的,如果在物件導向程式設計中一個類的函式提供了某種功能,那麼它要:
契約就是這些權利和義務的正式形式。我們可以用「三個問題」來總結DbC,並且作為設計者要經常問:
很多程式語言都有對這種斷言的支援。然而DbC認為這些契約對於軟體的正確性至關重要,它們應當是設計過程的一部分。實際上,DbC提倡首先寫斷言。
契約的概念擴充到了方法/過程的級別。對於一個方法的契約通常包含下面這些資訊:
繼承中的子類型可以弱化先驗條件(但不可以加強它們),並且可以加強後驗條件和不變式(但不能弱化它們)。這些原則很接近Liskov代換原則。
所有類之間的關係就是客戶與供應商的關係。一個客戶在呼叫供應商的功能時有義務不去違反供應商所需的狀態。相應的,供應商也有義務為客戶提供它所需的狀態和資料。例如,供應商的delete功能要求客戶在data buffer當中有資料存在。相應的,供應商要保證當delete功能完成後,data buffer中的資料已被刪除。其它的設計契約還有不變式。不變式保證類的狀態在任何功能被執行後都保持在一個可接受的狀態。
當使用契約時,供應商不應對契約條件是否被滿足進行校驗。大體的思想是,利用契約條件校驗為保護網,在契約被違反的情況下代碼會「硬性失敗」(fail hard)。DbC的「硬性失敗」概念讓對契約行為的除錯變簡單,因為每個過程的行為意圖被定義得很清楚。它和一種叫作防禦性編程的方法明顯不同,在那種方法裡,供應商要負責解決先驗條件不滿足的情況。相對通常的情況下,在DbC和防禦性編程中,如果客戶違反了先驗條件供應商都會丟擲異常—由客戶來負責解決這種情況。DbC讓供應商的工作更簡單。
DbC同時也定義了軟體模組的正確性條件:
因為契約條件在程式執行中不應被違反,它們可以只作為除錯代碼,或者在發布版本中被移除從而得到更好的效能。
DbC也能幫助代碼重用,因為每段代碼的契約都被很好的文件化了。模組的契約可以被當做軟體文件來描述模組的行為。
貫徹契約式設計特徵最多的語言套件含:
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.