契约式设计

<image>

契约式设计（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 2012
- Ciao (编程语言)
- Clojure
- Cobra (编程语言)
- D
- Dafny
- Eiffel
- Fortress (编程语言)
- Kotlin
- Mercury
- Oxygene (编程语言)（曾叫做Chrome和Delphi Prism）
- Racket
- Sather
- Scala
- SPARK（经过Ada程序的静态分析）
- Vala
- 维也纳开发方法

### 通过第三方支持的语言

- Ada，通过GNAT的先决条件和后置条件的pragma。
- Boost.Contract
- DBC for C预处理器
- GNU Nana
- eCv和eCv++ 形式验证工具
- Digital Mars C++编译器，通过C的CTESK扩展。
- Loki库，提供叫做ContractChecker的机制用来验证一个类服从契约设计。
- DBC C++
- C#（和其他.NET语言），通过Code Contracts
- Groovy，通过GContracts。
- Go，通过dbc或gocontracts
- OVal`[https://sebthom.github.io/oval/ OVal]`，经由AspectJ。
- Contracts for Java（Cofoja）
- Java建模语言（JML）
- Bean Validation（只有先决条件和后置条件）
- valid4j
- JavaScript，通过AspectJS（特别是AJS_Validator）、Cerny.js、ecmaDebug、jsContract、dbc-code-contracts或jscategory。
- Common Lisp，通过宏设施或CLOS元对象协议。
- Nemerle，通过宏。
- Nim，通过宏。
- Perl，通过CPAN模块Class::Contract（出自Damian Conway）或Carp::Datum（出自Raphael Manfredi）。
- PHP，通过PhpDeal、Praspel或Stuart Herbert的ContractLib。
- Python，使用包如deal、icontract、PyContracts、Decontractors、dpcontracts、zope.interface、PyDBC或Contracts for Python。
- Ruby，通过Brian McCallister的DesignByContract、Ruby DBC ruby-contract或contracts.ruby。
- Rust，通过contractscrate。
- Tcl，通过XOTcl面向对象扩展。

## 外部链接

- 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
- Bertrand Meyer, Applying "Design by Contract" , IEEE Computer, October 1992.
- Using Code Contracts for Safer Code