契约式设计

设计计算机软件的方法

契约式设计或者Design by Contract (DbC)是一种设计计算机软件的方法。这种方法要求软件设计者为软件组件定义正式的，精确的并且可验证的接口，这样，为传统的抽象数据类型又增加了先验条件、后验条件和不变式。这种方法的名字里用到的“契约”或者说“契约”是一种比喻，因为它和商业契约的情况有点类似。

定义

所谓契约，也就是合约，规定两个交互物件上的权利和责任。

雇佣合同规定你的工作时数和你必须遵守的行为规则，作为公司则付你薪水，双双履行义务，双双受益。

在应用程序中，Eiffel语言首先提供了《按契约设计》的概念，它关注的是用程序规定软件模块的权利和责任，以确保程序正确性。用文档记载权利和义务的说明，用程序来校验，这就是《契约式设计》的核心。Design by Contract（DbC，契约式设计）是面向对象软件大师Bertrand Meyer对软件构造方法的一个重大贡献，无论是在形式化的数学证明中，还是在实践运用中，都被证明是大幅改善软件工程质量的有效手段。该方法在Eiffel编程语言中获得直接支持，并且可以通过辅助工具在Java语言中运用。

因为Design by Contract是一个属于Eiffel Software的注册商标，很多开发人员用“Programming by Contract”, “Contract Programming”, 或者”Contract-First development“来指代这种方法。

描述

DbC的核心思想是对软件系统中的元素之间相互合作以及“责任”与“义务”的比喻。这种比喻从商业活动中“客户”与“供应商”达成“契约”而得来。例如：

1.供应商必须提供某种产品（责任），并且他有权期望客户已经付款（权利）。

2.客户必须付款（责任），并且有权得到产品（权利）。

3.契约双方必须履行那些对所有契约都有效的责任，如法律和规定等。

同样的，如果在面向对象程序设计中一个类的函数提供了某种功能，那么它要：

1.期望所有调用它的客户模块都保证一定的进入条件：这就是函数的先验条件—客户的义务和供应商的权利，这样它就不用去处理不满足先验条件的情况。

2.保证退出时给出特定的属性：这就是函数的后验条件—供应商的义务，显然也是客户的权利。

3.在进入时假定，并在退出时保持一些特定的属性：不变式。

契约就是这些权利和义务的正式形式。我们可以用“三个问题”来总结DbC，并且作为设计者要经常问：

1.它期望的是什么？

2.它要保证的是什么？

3.它要保持的是什么？

很多语言都有对这种断言的支持。然而DbC认为这些契约对于软件的正确性至关重要，它们应当是设计过程的一部分。实际上，DbC提倡首先写断言。

契约的概念扩展到了方法/过程的级别。对于一个方法的契约通常包含下面这些信息：

1.可接受和不可接受的值或类型，以及它们的含义

2.返回的值或类型，以及它们的含义

3.可能出现的错误以及异常情况的值和类型，以及它们的含义

4.副作用

5.先验条件

6.后验条件

7.不变式

8.(不太常见) 性能上的保证，如所用的时间和空间

继承中的子类型可以弱化先验条件（但不可以加强它们），并且可以加强后验条件和不变式（但不能弱化它们）。这些原则很接进Liskov代换原则。

所有类之间的关系就是客户与供应商的关系。一个客户在调用供应商的功能时有义务不去违反供应商所需的状态。相应的，供应商也有义务为客户提供它所需的状态和数据。例如，供应商的delete功能要求客户在data buffer当中有数据存在。相应的，供应商要保证当delete功能完成后，data buffer中的数据已被删除。其它的设计契约还有不变式。不变式保证类的状态在任何功能被执行后都保持在一个可接受的状态。

当使用契约时，供应商不应对契约条件是否被满足进行校验。大体的思想是，利用契约条件校验为保护网，在契约被违反的情况下代码要“死翘翘”（fail hard）。DbC的“死翘翘”概念让对契约行为的调试变简单，因为每个过程的行为意图被定义得很清楚。它和一种叫作defensive programming的方法明显不同，在那种方法里，供应商要负责解决先验条件不满足的情况。相对通常的情况下，在DbC和defensive programming中，如果客户违反了先验条件供应商都会抛出异常—由客户来负责解决这种情况。DbC让供应商的工作更简单。

DbC同时也定义了软件模块的正确性条件：

1.如果对一个供应商的调用之前类的不变式和先验条件是真，那么在调用后不变式和后验条件也为真。

2.当调用供应商时，软件模块应保证不违反供应商的先验条件。

因为契约条件在程序运行中不应被违反，它们可以只作为调试代码，或者在发布版本中被移除从而得到更好的性能。

DbC也能帮助代码重用，因为每段代码的契约都被很好的文档化了。模块的契约可以被当做软件文档来描述模块的行为。

对面向对象冲击

一 Server和Client的冲击：

程序库和组件库被类比为server，而使用程序库、组件库的程序被视为client。根据这种C/S关系，我们往往对库程序和组件的质量提出很严苛的要求，强迫它们承担本不应该由它们来承担的责任，引入契约观念之后，这种C/S关系被打破，大家都是平等的，你需要我正确提供服务，那么你必须满足我提出的条件，否则我没有义务“排除万难”地保证完成任务。

二权利和义务的关系：

一般认为在模块中检查错误状况并且上报，是模块本身的义务。而在契约体制下，对于契约的检查并非义务，实际上是在履行权利。一个义务，一个权利，差别极大。例如上面的代码：

if (dest == NULL) { ... }

这就是义务，其要点在于，一旦条件不满足，我方（义务方）必须负责以合适手法处理这尴尬局面，或者返回错误值，或者抛出异常。而：

assert(dest != NULL);

检查契约，履行权利。如果条件不满足，那么错误在对方而不在我

三确保必须条件：

契约所核查的，是“为保证正确性所必须满足的条件”，因此，当契约被破坏时，只表明一件事：软件系统中有bug。其意义是说，某些条件在到达我这里时，必须已经确保为“真”。

assert(dest != NULL);

报错时，你要做的不是去修改你的string_copy函数，而是要让任何代码在调用string_copy时确保dest指针不为空

四 “函数”和“过程”的理解：

我们以往对待“过程”或“函数”的理解是：完成某个计算任务的过程，这一看法只强调了其目标，没有强调其条件。引入契约之后，“过程”和“函数”被定义为：完成契约的过程。基于契约的相互性，如果这个契约的失败是因为其他模块未能履行契约，本过程只需报告，无需以任何其他方式做出反应。而真正的异常状况是“对方完全满足了契约，而我依然未能如约完成任务”的情形。这样以来，我们就给“异常”下了一个清晰、可行的定义。

三个关键词

一前置条件（precondition）：

为了调用函数，必须为真的条件，在其违反时，函数决不调用，传递好数据是调用者的责任。

二后置条件（postcondition）：

函数保证能做到的事情，函数完成时的状态，函数有这一事实表示它会结束，不会无休止的循环

三类不变项（class invariant）：

从调用者的角度来看，该条件总是为真，在函数的内部处理过程中，不变项可以为变，但在函数结束后，控制返回调用者时，不变项必须为真。

DbC六大原则

原则1 区分命令和查询。查询返回一个结果，但不改变对象的可见性质。命令改变对象的状态，但不返回结果。（应当是不一定返回结果）

原则 2 将基本查询同派生查询分开。派生查询可以用基本查询来定义。

原则 3 针对每个派生查询，设定一个后验条件，使用一个或多个基本查询的结果来定义它。这样我们只要知道基本查询的值，也就能知道派生查询的值。

原则 4 对于每个命令都撰写一个后验条件，规定每个基本查询的值。结合“用基本查询定义派生查询”的原则，我们已经能够知道每个命令的全部可视效果。