契约式设计

契约式设计（英語：，縮寫為 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++:
  • C#（和其他.NET语言），通过Code Contracts[7]
  • Groovy，通过GContracts。
  • Go，通过dbc[8]或gocontracts[9]
  • Java:
    • OValOVal，经由AspectJ。
    • Contracts for Java[10]（Cofoja）
    • Java建模语言（JML）
    • Bean Validation（只有先决条件和后置条件）[11]
    • valid4j （页面存档备份，存于）
  • 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面向对象扩展。

参考文献
  1. Bright, Walter. . Digital Mars. 2014-11-01 [2014-11-10]. （原始内容存档于2014-11-28）.
  2. Hodges, Nick. . Embarcadero Technologies. [20 January 2016]. （原始内容存档于2021-04-26）.
  3. Findler, Felleisen Contracts for Higher-Order Functions （页面存档备份，存于）
  4. . EPFL. [2019-05-24]. （原始内容存档于2019-12-25）.
  5. Strong typing as another "contract enforcing" in Scala, see discussion at scala-lang.org/ （页面存档备份，存于）.
  6. DBC C++ （页面存档备份，存于） Design by contract for C++
  7. . msdn.microsoft.com. [2022-03-02]. （原始内容存档于2022-06-04）.
  8. . [2022-03-02]. （原始内容存档于2022-06-04）.
  9. . [2022-03-02]. （原始内容存档于2022-06-03）.
  10. . [2022-03-02]. （原始内容存档于2022-03-03）.
  11. . beanvalidation.org. [2022-03-02]. （原始内容存档于2014-07-16）.
  12. . [2022-03-02]. （原始内容存档于2021-11-04）.
  13. . [2022-03-02]. （原始内容存档于2022-06-06）.
  14. . [2022-03-02]. （原始内容存档于2022-06-04）.
  15. . [2022-03-02]. （原始内容存档于2022-06-13）.
  16. . [2022-03-02]. （原始内容存档于2022-05-31）.

外部链接
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.