计算机编程/契约式设计

这篇文章关于 DbC 比其兄弟更关注契约式设计。原因是 Eiffel 的 DbC（以及极少数其他语言的 DbC）提供了与语言所有方面的完整 DbC 的紧密集成，以及语言的定义。

契约式设计

»没有我的抽象数据类型，不行！«

首先，契约式设计适用于模块、模块中的例程、子例程中的循环以及语句之间。异常也涉及其中。也就是说，你不能有部分契约。契约涉及在每个细化级别上的整个模块。

如果你建立了一个模块(!) 契约，契约的条款将应用于整个模块在其整个生命周期中。如果你使用一个有契约的模块，你就有义务遵守其可见规则。

模块有两种视图：客户端视图和供应商视图。当你编写一个子例程，并且该子例程调用包含在某个模块中的其他子例程时，你的子例程就变成了该模块的客户端。客户端看到模块契约的两个部分：

模块的不变式，以及
模块子例程的前置条件和后置条件。

从客户端的角度来看，模块本身被认为是供应商，它提供子例程。供应商看到更多模块，并添加一些内部契约条款，可以说。供应商必须提供，即编写：

模块的不变式，
模块子例程的前置条件和后置条件，
循环不变式和循环变体，
检查指令，
一致的异常处理。

所有这些都是断言，或者，在异常的情况下，与断言一致。

查看此处每个语言支持的设施： w:契约式设计.

断言

断言的目的是双重的：首先，它声明（计算的）变量及其关系的预期值。其次，它有助于测试变量是否具有声明的值，以及关系是否确实为真。作为程序的一部分，断言可以用作变量及其关系的运行时检查。但同时，断言允许在程序运行之前对其进行推理。你使用断言来证明一个模块、子例程、循环等是正确的。

每个断言都是一个布尔表达式，并且要么为True，要么为False。示例：

 $s=0$  or else  $g(s)=2*t$

示例中涉及两个变量的两个关系，一些值是计算出来的。两个相等测试要么为True，要么为False，并且通过或连接起来，这是一个布尔运算符。

如果将其应用于模块级别，断言可以表达客户端在调用模块子例程时必须满足的要求。这些要求以子例程的前置条件的形式声明，即涉及子例程形式参数以及可能模块的其他特征的断言。作为回报，子例程的后置条件描述了子例程将作为结果提供的服务。同样，后置条件是使用涉及子例程结果以及可能模块的其他特征的断言来表达的。典型的子例程描述，模块契约的一部分，可能如下所示：

  pop
        --  remove the topmost item
     require
        has_items: not is_empty
     ensure
        one_less: count = old count - 1

子例程pop不接受参数，也不返回任何内容。但是，它修改了模块，一个栈。因此，前置条件和后置条件是引用模块其他特征的断言，is_empty 和 count。有用的名称被附加到断言以供参考。

为了完成契约，在模块级别添加了另一个断言，模块不变式。模块不变式的关系通过说明在调用模块的子例程的每次调用之间保证了什么，来告知客户端模块的状态。示例：

 invariant
    sensible_count: count >= 0

契约违反是指评估为False 的断言。通常，当程序无法满足其断言时，会引发异常，因为程序显然是错误的。然后使用语言提供的异常机制来处理这种情况，并由契约式设计要求的规则约束。

在某些情况下，可以在编译时执行基于断言的广泛程序分析。这相当于机械地证明某些检查是不必要的。然后可以从编译后的程序中省略这些检查。请参阅 w:SPARK 编程语言.

如果断言为假，则程序中存在错误！

原因是程序没有根据断言产生应有的结果。以下是契约式设计中可能的断言列表（C 表示对客户端可见（模块外部），S 表示对供应商可见（模块内部））

模块不变式（C, S）: 模块不变式断言模块初始化后什么为真。它们还断言在执行其任何子程序之前和之后，相同的真值成立。
前置条件（C, S）: 子程序的前置条件声明在调用子程序之前必须为真。通常，它表达了（计算的）模块变量和子程序参数之间的关系。只有在前置条件为真时，子程序才能执行以满足其后置条件。
后置条件（C, S）: 后置条件声明子程序成功完成时（计算的）变量和关系将为真。
（循环变体）（S）: 循环变体是一个表达式（类型为自然数），其值在循环的每次迭代中都减小到零。通常使用循环中的一个变量来表达这种特性。循环变体保证了终止。
循环不变式（S）: 循环不变式表达一个关系，该关系在进入循环时或再次进入循环时为真。该关系将命名循环感兴趣的变量。
检查（S）: 当语句执行完毕后，它很可能通过赋值改变了若干变量的值。检查表达了程序员对赋值后这些变量之间关系的期望。

子程序的前置条件 P 和后置条件 QS从 Hoare 三元组的意义上构建子程序

{至少为 P} S {保证为 Q}，

前提是在调用之前和之后模块不变式为 True！注意最后一个要求。模块必须处于已知良好状态，因为前置条件和后置条件可能引用模块的状态。

契约式设计不是输入检查

按照推断，上面关于错误断言的规则意味着断言不能用来代替输入验证。当你不信任你的输入时，请在条件语句中使用你的语言提供的工具，例如 Ada 中的 'Valid 属性。例如，调用 Sqrt(x)，其中 x = -1.23，这是使用Sqrt的一个错误，违反了契约。调用者没有在将 x 发送到数学例程之前测试 x。

断言不能代替条件语句

你能将各种数字传递给Sqrt，并只准备处理当Sqrt的前置条件评估为 false 时引发的异常吗？换句话说，你能故意无视契约吗？答案是否定的，至少有两个原因。

如果一个模块已被证明是正确的，则断言检查可能已被关闭，期望客户端会履行其契约义务。调用者的契约违反可能会被忽视，并可能产生巨大的错误计算。
如果被调用的子程序不是Sqrt，而是控制火车的速度，你不能只是传递无效输入，直到它没有使速度控制子程序因异常而失败。更糟糕的是，请参阅 1。

示例：栈

（这个例子是用非常简化的 Ada 符号给出的，知道 Ada 2005 中的 DbC 支持非常好，但有限制。想象一下，将 require、ensure 和 invariant 替换为标记为pre, post和inv的注释，将使以下内容更接近 Eiffel 原版。使用你的语言提供的工具来表达断言和异常处理。）

下面的感叹号（`!'）只是一个符号。它们代表各个语言提供的工具。它们的含义只是契约的信息。

generic
   type Item is private;
   --  any definite type that permits assignment

package Stack is

   --  last in first out storage, initially empty

   function is_empty return Boolean;
   --  is there an element on the stack?
   --  ! post: result = (count = 0)

   function count return Natural;
   --  number of items currently on the stack

   function top return Item;
   --  the topmost item
   --  ! pre: not is_empty

   procedure push(x: Item);
   --  add `x` on top of the stack
   --  ! post: count = old count + 1
   --  ! post: not is_empty
   --  ! post: top = x

   procedure pop;
   --  remove the topmost item
   --  ! pre: not is_empty
   --  ! post: count = old count - 1


   --  ! inv: count >= 0
   --  ! inv: (count = 0) = is_empty

end Stack;

请注意，到目前为止，模块中还没有可执行语句。它只是一个包含契约式先决条件和后置条件以及模块不变式的包规范。然而，就该模块的客户端而言，模块的契约是完整的。

top 函数的先决条件声明堆栈上必须存在元素，否则它无法成功。为了表达这一点，它引用了同一个模块中的另一个函数 is_empty。注意模块不变式允许空堆栈。count 函数既没有先决条件也没有后置条件，但它在模块不变式中被提及。这意味着客户端仍然可以预期 count 返回一个 >= 0 的值。

现在，如果 is_empty = False，那么根据 count >= 0，count > 0 必须为真，因为not is_empty 当且仅当 count /= 0。

如果您最终使用语言定义中的断言和规则证明软件组件，那么该组件就符合这些契约的意义。

模块的内部视图，在本例中是包体，展示了如何在程序中放置断言。重要的是要理解pragma assert 在 Ada 中，require 在 Eiffel 中，等等，与语言的异常处理机制紧密集成。这与您可能从 C 的 assert 中推测的情况不同。（示例堆栈的实现实际上是基于 Ada.Containers，类似于 Eiffel 的 STACK 类通常是如何实现的。它也可以基于 D 的 arrays，或者您选择的任何语言。）

pragma Assertion_Policy(Check);
  ...
   s: Vector;
  ...
   function top return Item is
   begin
      pragma assert(not is_empty, "stack is empty");
      return s.Last_Element;
   end top;

考虑一下打开或关闭断言检查的效果。断言表达契约，它们不处理无效输入。

异常和契约

如果先决条件为真，但正在执行的子程序中的某些语句引发了异常，会发生什么？很有可能子程序无法再建立后置条件。它将失败。但是，模块的状态如何呢？

关于模块状态的第一个答案由以下规则给出

当允许异常从子程序传播时，必须首先建立模块不变式。

第二个答案可能不同，具体取决于语言。例如，Eiffel 的方式是在发生异常的情况下重试例程：如果异常被处理，并且子程序应该重试以满足其后置条件，那么它的先决条件和模块不变式必须首先被建立。（否则，系统无法在不违反契约的情况下像再次调用例程那样工作。）

Ada 与其他一些语言一样，具有嵌套块，因此异常处理可以从块的先决条件开始。因此，如果您设法恢复块的先决条件，就可以重试该块。例如，一个块可以嵌套在循环内部。然后，您的处理程序将必须将满足循环执行所需先决条件的值分配给变量。

继承

待定

简而言之，被覆盖方法的先决条件是或运算的，后置条件是与运算的。

对于围绕派生类型构建的模块，必须能够用派生类型的对象替换父类型的对象，以便调度调用仍然可以依赖父类的契约。同样，实际调用的特征的后置条件必须暗示父特征的后置条件。

一个缺陷

给定一个 OO 父类型 T，以及它的其中一个方法，

 type T is tagged private;

 function foo(x: T; n: Count) return Natural;
 -- ! pre: n >= 42

以及一个从 T 派生的类型 D，该类型的方法被覆盖，

 type D is new T with private;
 
 overriding
 function foo(x: D; n: Count) return Natural;
 -- ! pre: n >= 66

想象一下，T 层次结构中某个类型的一个 OO 变量的引用。然后

 declare
     x: access T'Class := new D;
 begin
     x.foo(42);
 end;

谁该负责呢？

并发

待定

并发执行引入的一个新问题（到目前为止）是：假设

模块的例程应该代表多个调用者完成工作，
某个例程的“实例”可能会被另一个“实例”中断

那么，例如，在第一个调用启动时模块状态为真的情况可能在执行第二个调用更改了模块状态后不再为真。这扩展到先决条件/后置条件检查：由于例程的断言很可能引用它们的模块状态（以及一般可见的任何内容），因此它们可能会变得不一致。

第一个解决方案尝试是使先决条件检查、例程的执行以及后置条件检查顺序和排他。也就是说，只要一个调用者正在接受例程的服务，对该例程的其他调用将处于挂起状态，直到该例程完成。

但此外，由于例程的断言是关于模块状态的，因此任何其他调用者调用的模块服务都应该被暂停。

另请参阅守卫、SCOOP、Ada（任务和受保护类型、同步接口）。

另请参阅

Gries, David (1981)，编程的科学。纽约

Findler, Robert Bruce；Latendresse, Mario；Felleisen, Matthias (2001)，行为契约和行为子类型。http://doi.acm.org/10.1145/503209.503240 或 http://www.ccs.neu.edu/scheme/pubs/fse01-flf.pdf

Hoare, C. A. R. (1969)，计算机编程的公理基础。CACM，第 12 卷，第 10 号，第 576-583 页。http://doi.acm.org/10.1145/357980.358001 ，http://doi.acm.org/10.1145/363235.363259

Liskov, Barbara H.；Wing, Jeannete M.，子类型的行为概念。 http://doi.acm.org/10.1145/197320.197383 或 http://www.cs.cmu.edu/afs/cs.cmu.edu/project/venari/papers/subtype-toplas/paper.ps

Meyer, Bertrand (1997)，面向对象软件构建（OOSC2）。新泽西。第 11 章。

http://www.ecma-international.org/publications/standards/Ecma-367.htm

w:契约式设计

（当然，还有 Dijkstra）