契約式設計
契約式設計（英語：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也能幫助代碼重用，因為每段代碼的契約都被很好的文件化了。模組的契約可以被當做軟件文件來描述模組的行為。
語言支援
[編輯]原生支援語言
[編輯]貫徹契約式設計特徵最多的語言套件含：
通過第三方支援的語言
[編輯]- Ada，通過GNAT的先決條件和後置條件的pragma。
- C和C++:
- Boost.Contract （頁面存檔備份，存於互聯網檔案館）
- DBC for C預處理器
- GNU Nana
- eCv和eCv++ 形式驗證工具
- Digital Mars C++編譯器，通過C的CTESK擴充。
- Loki庫，提供叫做ContractChecker的機制用來驗證一個類服從契約設計。
- DBC C++[6]
- C#（和其他.NET語言），通過Code Contracts[7]
- Groovy，通過GContracts。
- Go，通過dbc[8]或gocontracts[9]
- Java:
- JavaScript，通過AspectJS（特別是AJS_Validator）、Cerny.js、ecmaDebug、jsContract、dbc-code-contracts[12]或jscategory。
- Common Lisp，通過宏設施或CLOS元對象協定。
- Nemerle，通過宏。
- Nim，通過宏[13]。
- Perl，通過CPAN模組Class::Contract（出自Damian Conway）或Carp::Datum（出自Raphael Manfredi）。
- PHP，通過PhpDeal[14]、Praspel或Stuart Herbert的ContractLib。
- Python，使用包如deal[15]、icontract、PyContracts、Decontractors、dpcontracts、zope.interface、PyDBC或Contracts for Python。
- Ruby，通過Brian McCallister的DesignByContract、Ruby DBC ruby-contract或contracts.ruby。
- Rust，通過contracts[16] crate。
- Tcl，通過XOTcl物件導向擴充。
參考文獻
[編輯]- ^ Bright, Walter. D Programming Language, Contract Programming. Digital Mars. 2014-11-01 [2014-11-10]. （原始內容存檔於2014-11-28）.
- ^ Hodges, Nick. Write Cleaner, Higher Quality Code with Class Contracts in Delphi Prism. Embarcadero Technologies. [20 January 2016]. （原始內容存檔於2021-04-26）.
- ^ Findler, Felleisen Contracts for Higher-Order Functions （頁面存檔備份，存於互聯網檔案館）
- ^ Scala Standard Library Docs - Assertions. EPFL. [2019-05-24]. （原始內容存檔於2019-12-25）.
- ^ Strong typing as another "contract enforcing" in Scala, see discussion at scala-lang.org/ （頁面存檔備份，存於互聯網檔案館）.
- ^ DBC C++ （頁面存檔備份，存於互聯網檔案館） Design by contract for C++
- ^ Code Contracts. msdn.microsoft.com. [2022-03-02]. （原始內容存檔於2022-06-04）.
- ^ dbc. [2022-03-02]. （原始內容存檔於2022-06-04）.
- ^ gocontracts. [2022-03-02]. （原始內容存檔於2022-06-03）.
- ^ Contracts for Java. [2022-03-02]. （原始內容存檔於2022-03-03）.
- ^ Bean Validation specification. beanvalidation.org. [2022-03-02]. （原始內容存檔於2014-07-16）.
- ^ dbc-code-contracts. [2022-03-02]. （原始內容存檔於2021-11-04）.
- ^ macros. [2022-03-02]. （原始內容存檔於2022-06-06）.
- ^ PhpDeal. [2022-03-02]. （原始內容存檔於2022-06-04）.
- ^ deal. [2022-03-02]. （原始內容存檔於2022-06-13）.
- ^ contracts. [2022-03-02]. （原始內容存檔於2022-05-31）.
外部連結
[編輯]- The Power of Design by Contract(TM) （頁面存檔備份，存於互聯網檔案館） A top-level description of DbC, with links to additional resources.
- Building bug-free O-O software: An introduction to Design by Contract(TM) （頁面存檔備份，存於互聯網檔案館） Older material on DbC.
- Benefits and drawbacks; implementation in RPS-Obix Archive.is的存檔，存檔日期2013-02-01
- Bertrand Meyer, Applying "Design by Contract" （頁面存檔備份，存於互聯網檔案館）, IEEE Computer, October 1992.
- Using Code Contracts for Safer Code （頁面存檔備份，存於互聯網檔案館）