计算机编程/契约式设计

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

契约式设计

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

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

如果你设置了一个模块(!)契约，契约的条款将适用于整个模块在其整个生命周期中。如果你使用一个有契约的模块，你必须遵守其可见规则。

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

1. 模块的不变式和
2. 模块子例程的前置条件和后置条件。

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

1. 模块的不变式,
2. 模块子例程的前置条件和后置条件,
3. 循环不变式和循环变量,
4. 检查指令
5. 一致的异常处理

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

检查每个语言提供的支持功能：w:Design by contract.

断言

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

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

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

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

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

  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 programming language.

---

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

---

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

模块不变式 (C, S)

模块不变式断言模块初始化后什么为真。它们还断言在执行其任何子程序之前和之后，相同的真值保持不变。

前置条件 (C, S)

子程序的前置条件声明在调用子程序之前什么必须为真。通常，它表达（计算的）模块变量和子程序参数的关系。只有当前置条件为真时，子程序才能执行以满足其后置条件。

后置条件 (C, S)

后置条件声明子程序成功完成后，（计算的）变量和关系将为真。

(循环变量) (S)

循环变量是一个表达式（类型为 Natural），其值在循环的每次迭代中都减少到零。通常，循环中的一个变量被用来表达这个属性。循环变量保证终止。

循环不变式 (S)

循环不变式表达一个关系，该关系在进入循环时或再次进入循环时为真。该关系将命名与循环相关的变量。

检查 (S)

当一条语句执行完毕后，它很可能会通过赋值改变一个或多个变量的值。检查表达了程序员对这些变量在赋值之后的关系的预期。

子程序的前置条件 P 和后置条件 QS从Hoare 三元组的角度来说，对子程序进行了限定

{至少 P} S {保证 Q},

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

契约式设计不是输入检查

从上面的关于错误断言的规则中，可以推断出，断言不应作为输入验证的替代。当你不信任你的输入时，请使用你的语言提供的条件语句中的方法，例如 Ada 中的'Valid属性。例如，调用 Sqrt（x）其中 x = -1.23 是使用Sqrt的错误，违反了契约。调用者在将 x 发送到数学例程之前，没有对其进行测试。

断言不能替代条件语句

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

1. 如果一个模块被证明是正确的，则可以关闭该模块的断言检查，预计客户端将履行其契约义务。调用者违反契约可能会不被察觉，并可能导致严重错误的计算。
2. 如果调用的子程序不是Sqrt而是控制火车的速度，你不能一直传递无效的输入，直到它碰巧没有使速度控制子程序因异常而失败。更糟糕的是，见 1。

示例：堆栈

(这个示例是用非常简化的 Ada 符号表示的，因为知道 Ada 2005 中对 DbC 的语言支持相当好，尤其是在 Ada 2005 中，但有限。想象一下，将 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;

谁该负责？

并发

待定

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

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

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

第一个解决方案尝试是使前置条件检查、例程的执行和后置条件检查顺序且排他。也就是说，只要调用者由例程服务，对例程的其他调用就会处于挂起状态，直到例程完成为止。

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

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

另请参阅

Gries, David (1981), The Science of Programming. New York

Findler, Robert Bruce; Latendresse, Mario; Felleisen, Matthias (2001), Behavioral Contracts and Behavioral Subtyping. http://doi.acm.org/10.1145/503209.503240 或 http://www.ccs.neu.edu/scheme/pubs/fse01-flf.pdf

Hoare, C. A. R. (1969), An Axiomatic Basis for Computer Programming. CACM, Vol.12, Number 10, pp. 576–583. http://doi.acm.org/10.1145/357980.358001 , http://doi.acm.org/10.1145/363235.363259

Liskov, Barbara H.; Wing, Jeannete M., A Behavioral Notion of Subtyping. 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), Object Oriented Software Construction (OOSC2). New Jersey. Chapter 11.

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

w:Design by contract

（当然，还有 Dijkstra）