契約式設計
契約式設計（英語：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 （頁面存檔備份，存於網際網路檔案館）
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||