契约式设计引论 --建造无错软件

感谢译者的辛勤付出，更感谢原作者的智慧共享。

译文转载自：http://softwarepractitioner.org/translations/meyer/contract.shtml

=========================================================================

 

概  述

「契约式设计」的概念是OO软件系统化构建方法的中心所在，此概念已深植于Eiffel方法中。这篇文章阐述契约式设计的一些关键思想。

我们认为本文中介绍的技术与O－O技术的其他概念，如类、物体/对象、继承性、多态性以及动态连接 同样重要，尽管至今只有少量的O-O文献专门论及于此。（见此文的参考文献 ）。

阅读本文能从理论上理解这种方法，如果要获得这种方法的实际经验，请看 Eiffel环境 ，它直接实现了本文提到的这些思想。

 

注意 ：郑重提醒一下不遵循本文所阐述的原则的实际后果，请看 Put it in the Contract: The Lessons of Ariane （这篇文章原载于IEEE Computer ）。

 

1 - 导论

许多人在考虑软件开发的新方法和新工具时，都是把提高生产率 或产量 （productivity ）作为主要的期望目标。 在O-O技术中，特别是在Eiffel中，产量不仅直接受益于方法途径，也受益于对质量的重视。用NEC的 Software Development Group的副总裁K. Fujino的话来说：

 

• 质量当头，产量其中（When quality is pursued, productivity follows〕

• (引自Carlo Ghezzi, Dino Mandrioli和Mehdi Jazayeri所著 软件工程（Software Engineering） , Prentice Hall 1991.)

软件质量的一个主要部分是可靠性（reliability）：系统要能够完成所规定的任务（ 正确性 －－ correctness ），也要能够妥善处理异常情况（稳固性 －－ robustness ）。 一句话，可靠性就是系统没有错误故障。

 

软件开发不管是用什么方法途径，一般都对可靠性有很高的要求。而在O-O方法中，可靠性尤其重要， 这是因为O-O方法中复用性（reusability）扮演着特殊的角色：除非我们得到的可复用的软件部件 其正确性远高于一般的软件，复用只是一桩赔本买卖。

 

我们如何来建造可靠的O-O软件呢？答案有几个部分。Static typing（静态类型严格兼容） 能够帮助我们及早抓住源码中那些 不一致的部分，从而避免使其成为故障之源。Garbage collection（无用存储单元收集）， 尽管有时被认为是属于实现的层次而被 排除在外，实际上也是很基本的，因为它从根本上避免了进行存储器管理时容易犯的错误。 复用也是很有用的：如果你能复用那些由信誉良好的机构开发并验证的软件部件， 而不是对你遇到的每一个问题 都自己开发解决方案，你就能开始信任你部分的软件，就象你信任你运行软件的机器一样。这样， 可复用的程序部件库就变成了硬－软机器（硬件，操作系统，编译器）的一部分。

 

但这还不够。要确定地让我们的O-O软件系统正确地运行，我们需要一个系统的方法来描述和 实现O-O软件单元以及它们在系统中的关系。本文就是介绍这样一种方法，称之为Design by Contract （契约式设计）。在契约式设计的理论中，一个软件系统被视为一组相互交流的部件，它们之间 互动的基础是一组准确定义了的规范，它规定了这些部件相互之间的义务 －－ 即契约。

 

契约式设计有如下一些好处：

 

• 它让人更好地理解O-O方法和软件构造。
• 它是一种系统化的建造无错O-O软件的方法。
• 它为除错、测试、和更一般的质量保证提供了一个有效的框架。
• 它是一种给软件部件建立文档的方法。
• 它能让人更好地理解和控制继承（inheritance）机制。
• 它是一种能安全有效地处理异常情况的技术。

下面阐述的思想是Eiffel 的一部分[1 , 3 ]， 但这里希望读者不要把它只看成是一个编程语言，而是应把它作为一种软件开发的方法。

 

2 - 规范与排错

要提高软件的可靠性，首要的、也许是最困难的问题是，对每一个软件单元都要尽可能准确地 定义期望它们干什么。这马上会招来反对意见：准确定义一个模块的规范并不能保证这个 模块就能作到规范所定义的事。当然，这种意见是对的，但是：

 

• 其实这个意见也可以换种说法。 你会注意到我们只是说一个模块应该做 什么，这和这个模块要去做 没什么关系 （这里没有奇迹发生）。
• 实践中，常会令人惊奇的看到，本来仅仅是要求表述一个模块应该做什么，结果却是在往确保 这个模块去做这个方向上走，还走得很远。

下面你可以看到，尽管规范说明不能完全保证一个模块的正确性，但它为系统化的测试和 排错提供了一个良好的基础。

 

契约式设计理论建议每一个软件单元都应该有一个规范说明。这些规范（或契约）管理着 一个软件单元与其外部世界的交互活动。

 

这里所说的规范并不是说使用完全形式化规范方法。尽管一般来说，形式化规范是很有 吸引力的，但是我们这里的规范说明并不一定要求是穷尽的。这有利于把规范语言嵌入到设计 和编程语言中（如Eiffel），而典型的形式化规范语言一般是不可执行的，或者即使可执行， 目前也只能用于实验原型。我们这里的标准更高一些：我们需要作有效的系统实现。这样保 持了无缝性（seamlessness） 这个O-O软件开发过程的特性，即是说，在软件的整个 开发周期中，从分析到实现再到维护，可以只使用一套标识符和概念。这样能保证问题和解决 方案之间更好的映射，从而得到更好的系统演进和其他一些益处。

 

3 - 契约概念

在人类的社会活动中，契约一般是用于两方，一方（供应者）为另一方（客户）完成一些任务。 每一方都期待从契约中获得利益，同时也要接受一些义务。通常，一方视为义务的对另一方来说 是权利。契约文档要清楚地写明双方的权利与义务。

我们可以用表格来方便地描述一个契约，如下表列出了一个航空公司和乘客的契约：

 

义 务 权 利

客 户	（必须保证的前提条件） 至少比起飞时间提前5分钟到达Santa Barbara机场。只携带许可的行李。票价已付。	（可以得之于后置条件) 到达Chicago。
供 应 者	（必须保证的后置条件） 把乘客运到Chicago。	(可以假设的前提条件) 对于那些迟到的、携带不合规定行李的、或没有付票价的乘客，可以不予运载。

 

契约合同能保障双方的利益，对客户来说，合同规定了供应者要做的工作；对供应者来说， 合同说明了如果约定的条件不满足，供应者没有义务一定要完成规定的任务。

 

同样的道理也适合于软件。设想一个软件单元E 。它要达到它的目的（履行契约）， E 使用的策略可能会包括一系列的子任务，t1 , ... tn 。如果子任务ti 不是那么简单的，它得调用另一个功能例程（routine)R 。换句话说，E 把子任务 转包给R 。这样的情形应该被一个很好定义的“登记表”(roster）来管理双方的义务与权利 －－契约。

 

假如ti 是一项任务，要求把一个给定的元素插入到一个 有限容量的字典中。此处字典是一个（名－值）表，每一个元素（值）通过一个作为关键字的字 符串（名）存取。（译者注：这里“元素”可以理解成一个任意的数据项）

 

义务 权利

客 户	(必须保证前提条件）   确保这张表没满并且关键字非空。	（可以得之于后置条件) 得到一张更新后的表，其中含有给定的元素并且与给定的关键字相连配对。
供 应 者	（必须保证后置条件） 将给定的元素记录在表中，并使其与给定的关键字相连配对。	（可以假定的前提条件） 如果表满了或关键字串为空，则可什么都不做。

 

这个契约规约着功能例程（routine）和这个例程的调用者的关系。它包含着关于这个功能例程 的最重要的信息：要完成一个正确的调用，契约中的各方必须要保证什么；作为回报， 各方有权获得什么。

 

这个信息非常重要，如果它只是停留在象上面这样的非正式描述上，那么显然是不能令人满意的。 依照“无缝性”（seamlessness）精神（即鼓励我们把所有层次上的所有相关信息都放在一个软件 文本中），我们应该为这个功能例程的文本（译者注：此处文本可大概理解成源码）装备上一组合适 的条件。假设这个功能例程称为“put ”，是一个通用类 DICTIONARY [ELEMENT ]的一部分，则可用Eiffel语言表述如下：

 

     put (x: ELEMENT; key: STRING) is
                     -- Insert x so that it will be retrievable through key.
             require
                     count <= capacity
                     not key.empty
             do
                     ... Some insertion algorithm ...
             ensure
                     has (x)
                     item (key) = x
                     count = old count + 1
             end

 

 

require 子句引出了输入条件，或前提条件（precondition）； ensure 引出了输出条件，或后置条件（postcondition）。 这两个条件都是与软件单元（译者注：此处为DICTIONARY [ELEMENT ]） 相关联的断言（assertion），或逻辑条件（契约子句）。 在前提条件中，count 是当前数据项的数量，capacity 是允许的最大数； 在后置条件中，has 是个布尔查询，它告诉你一个给定的元素是否存在， 而item 的结果是一个与指定关键名相连的元素；old count 表示进入put 时的count 值。

 

4 - 分析中的契约

上面的例子取自于一个功能例程的实现（尽管事实上“字典”的概念与任何具体实现无关）。 但是这里阐述的思想在分析这个层次上也是很有意思的。例如，设想一个化学工厂模型，其中的类 可以有TANK , PIPE , VALVE , CONTROL_ROOM 。 每一个类都描述了一个特定的数据抽象－－一个现实世界中一类物体/对象，其性质由一组特征 （feature）或操作（operation）所表达（译者注：feature可视为Java中的method，与作者用的 routine基本同义）。 例如，TANK 可以有下列的特征（feature）：

 

• Yes/no 查询: is_empty, is_full...
• 其他查询: in_valve, out_valve (both of type VALVE ), gauge_reading , capacity ...
• 命令: fill, empty, ...

Then to characterize a command such as fill we may use a precondition and postcondition as above:

要具体描述一个命令的特性，如fill ，我们可以用前提条件（precondition）和后置条件（postcondition）：

 

        fill is
                        -- Fill tank with liquid
                require
                        in_valve.open
                        out_valve.closed


                deferred             -- i.e., no implementation


                ensure
                        in_valve.closed
                        out_valve.closed
                        is_full
                end 

 

这种风格的分析避免了分析和规范的一个经典的两难处境：或者你使用编程标识符，其风险是过早 地开始实现工作；或者你得使用高层次的标识系统（泡泡加箭头），但必须保持模糊性，而这被认为是分析 过程的主要好处之一，即能够表述并进一步细化系统的属性。而在我们这里，标识符号是精确的（感谢断言 机制，它可以用来表述许多操作的语义），但又避免了实现细节。（上面例子中介绍的方法是没有危险的， 因为此时我们给出的描述还不包括软件和计算机！这里我们只是把这套标识符用来作为建模工具而已）。

 

Waldén 和Nerson在[5 ]中提出的 Business Object Notation 是目前仅有的一种完全整合了分析和设计层次的O-O方法，它提供的一套图形标识符号实现了本文所 提出的思想。

 

5 - 不变条件（Invariants）

前提和后置条件适用于功能例程（routine）。我们可以其他断言来描述整个类（class）的 特点。如果一个断言表述了一个类的所有个体（instance）都要满足的条件，则此断言称为 “类不变条件”（class invariant ）。例如，DICTIONARY 这个类的不变条件 可表述为：

 

        invariant
                0 <= count
                count <= capacity

 

TANK 的不变条件可表述为：is_full 是指“近似满”:

 

        invariant
                is_full = (0.97 * capacity <= gauge) and
                                 gauge <= 1.03 * capacity)
           ... Other clauses ...

 

“类不变条件”是一组保持一致性的限制条件，它表达了一个类的语义特性。这个概念对配置管理 （configuration management）和回归测试（regression testing）都是很重要的，因为它描述了一个类的更 深的属性：不仅仅是它的演进中某一点的特性，还有在它发生变化时必须满足的限制条件。

 

从契约理论来看，一个不变条件是这样一个总体子句（general clause)，它制约着所有那些 用来描述一个类的契约。

 

6 - 文档

契约式设计的另一个关键应用是提供了一个标准方法来给类这个软件单元建立文档。一个类要为客户 （使用者）所 正确使用，那么它的接口属性应该提供给客户方的程序员。通常，一个类的接口属性的描述可用一种 简短形式 ，即去掉了这个类所有的实现信息而只保留了使用信息：契约。

 

在EiffelBench环境 中, 点击Class Tool上的的Short按钮，你就可以得到一个类的简短描述。输出结果可以是简单文本 （plain text），也可转换成其他格式的文本（Microsoft's RTF, 用于Web的HTML, 用于 FrameMaker的MIF或MML，以及TEX，troff，Postscript等等）。转换是通过EiffelBench环境预先 提供的一组“过滤器”（filter）来实现的，你也可以加上你自己的过滤器，因为这个结构机制是完全 开放的。

 

简短描述只保留了外部特征功能（exported feature）（译者注：类似Java中的public method） 的标题和断言（precondition & postcondition），以及不变条件，而去掉了其他所有的东西。

 

  class interface DICTIONARY [ELEMENT] feature
   put (x: ELEMENT; key: STRING) is
            -- Insert x so that it will be retrievable
                           -- through key.
                  require
                          count <= capacity
                          not key.empty
                   ensure
                          has (x)
                          item (key) = x
                          count = old count + 1
                ... Interface specifications of other features ...
  invariant
                0 <= count
                count <= capacity
  end -- class interface DICTIONARY  

 

这种简短描述可用来为程序库和其他软件单元建文档。它也可作为开发人员间的中心交流工具。 从客户以及我们自己的经验中，我们认为这种简短描述大大有利于软件设计与项目管理，因为它 鼓励开发人员与管理人员讨论那些关键问题（接口，规范，模块间规程），而不是内部实现细节。

 

7 - 测试、排错、质量保证

对一个类来说，如果它的描述文本带有断言，我们最好应当能够从数学上证明一个特征功能（feature） 的实现是满足给出的断言的。但现在还没有工具能做到这一点，这种情况下，我们所能做的最好 的就是用断言来作测试。

 

对每一个类来说，如何使用它的断言（如果有的话），可以由开发人员通过设置编译选项来决定： 无断言检查（断言无任何效用，仅作为标准化的注释），只查前提条件（此为系统设置值）， 前提与后置条件，所有前面这些加上类不变条件，或所有断言。

 

这些机制提供了一套非常有效的工具以搜寻错误。断言监测这种方式可以查验软件是否 确如其作者所设想的那样工作，这是一条进行排错、测试和质量保证的非常有效的途径， 因为错误搜寻不是盲目的，而是基于开发者自己提供的一致性条件来进行的。

 

从我的经验来看，这种技术的最主要的特点之一便是提供了这种排错机制。它能极大地减少 错误的数量，并且能让开发人员以一种新的眼光来看软件可靠性。

 

8 - 契约与继承

契约式设计理论的一个重要结果是使人能更好地理解O-O中的inheritance（继承性），polymorphism （多态性），redefinition（重定义）与dynamic binding（动态连接）。

 

假定有class B 继承class A ，B 可以对某一个继承于A 的 特征（feature）r 重新予以定义。例如，DICTIONARY 的一个特定的实现 可以重新定义put 算法。但是，这样的重新定义是有潜在危险的，因为原则上新的定义可能 具有完全不同的语义。这一点很值得忧虑，特别是在多态性（polymorphism）存在的情况下。 考虑如下调用

 

  a.r

 

调用目标a 的静态类型是A ，但运行时它可以表示一个具有类型B 的物体/对象。 那么动态连接（dynamic binding）意味着B 定义的r 版本将会被调用。

 

这种情形便是“合同转包”（subcontracting）：A 把任务 r 转包给 B 。但“转包承接者”（subcontractor）（这里是B ）必须要受原合同的制约。

 

     if a.pre then
             a.r
     end

 

契约允诺的结果必须要得以保证：因为前提条件满足，调用将会正确执行（假定pre 蕴涵着r 的前提条件）；退出时 a.post 将为真，此处post 是r 的后置条件。

 

“契约转包”原则得之于下面这些观察：r 的一个重新定义的版本需保持或弱化 前提条件，而需保持或强化后置条件。强化前提条件或弱化后置条件实际上是 “不诚实转包”（dishonest subcontracting），会导致灾难性后果。Eiffel语言中对于 断言重定义的规则支持“契约转包”原则。（译者注：对转包承接者来说，给他的条件和原合同 相同或更差，而要他出的活要达到或超过原合同的要求。）

 

这些观察深刻地揭示了继承的重要性：不仅仅是一种复用和分类/型的机制，其语义 兼容也应该并且可以通过一些手段得以保证。这些原则也可用来指导如何妥善地使用继承 性（inheritance）。

 

9 - 异常处理

在契约理论的许多应用中，一个重要的应用就是它能引导我们自然而然地推出一种系统化的途径 来处理一个很头疼的问题－－异常情形处理。

 

一个软件单元总是能以一定的方式来履行它的契约，这可以是也可以不是那么显而易见的。 一个异常情形是 指一个软件单元不能履行它的契约，这可以有多种原因：发生硬件故障，调用的一个例程失败， 或有软件错误使得它不能完成契约。

 

在这样的情形下，只有三种处理方式有意义：

 

1. 再试 ：有可替换的策略可用。程序将恢复不变条件，然后用新的策略再试试。

2. 忙而不乱（organized panic） : 无可替换的策略可用。则恢复不变条件，终止， 然后产生一个新的异常情形来向调用者报告这个失败。

3. 假警报 ：事实上，如果采取一些措施之后，程序可继续运行。这种情形很少发生 （非常遗憾，因为这是最容易实现的）。

异常处理机制直接建立在这样的分析上。在Eiffel中，一个功能例程程（routine）可以有 “rescue”子句和“retry”指令。这类似于人类合同中的相应条款，即允许异常的、没 计划到的情况发生。如果程序中有“rescue”子句，那么在运行中发生的异常将中断正常 运行（do 子句），而启动运行rescue子句。Rescue子句可以有一或多条指令； 其中之一是retry ，它将使do 子句再执行一遍。一个整型局部变量，如 failure 总是在进入该功能例程程时被清零（当然不会在retry 后再清零）。

 

这有一个例子可演示这个机制（详见[2, 3]）。我们假设有个低级例程unsafe_transmit 用来在网络中发送数据。我们不能控制unsafe_transmit ，但是知道它可能会失败， 如果失败，我们想再试试，最多100次，还不成功就把一个异常回送给我们的调用者。Rescue/Retry 机制能简单又直接地支持这个要求：

 

     attempt_transmission (message: STRING) is
                   -- Attempt to transmit message over a communication line
                   -- using the low-level (e.g. C) procedure unsafe_transmit,
                   -- which may fail, triggering an exception.
                   -- After 100 unsuccessful attempts, give up (triggering
                   -- an exception in the caller).
           local
                   failures: INTEGER
           do
                   unsafe_transmit (message)
           rescue
                   failures := failures + 1
                   if failures < 100 then
                      retry
                   end
           end

 

10 - 进一步的发展

这篇文章概要地阐述了契约式设计的基本思想。这是一个很活跃的领域，进一步的研究在进行中， 还有几本书的出版也在准备中。这里简单提一下契约式设计在两个方面的研究进展：

 

• 并行与分布 ：契约式设计原则对解决并行和分布式OO程序设计中的问题提供了 令人鼓舞的方法（避免了所谓的“继承性不规则”（inheritance anomaly），以及其他OO并行 计算的问题，这些问题都是由于没能正确理解O-O技术所引起），详见 另一篇文章 。 参考文献[4]详细描述了Eiffel系统如何基于契约式设计理论来作并行计算的，这些在 ISE Eiffel 4.2中正在予以实现（最新阐述见[1]的新版）。
• 扩充的规范语言 ，提供了更丰富的断言表达。

契约式设计已经被广泛应用；这个理论对使用O-O方法提供了一条强有力的思路，它涉及了在 应用O-O技术和语言时遇到的许多问题，如：需要用一套什么样的方法过程，应该用什么概念作 为分析阶段的基础，如何为O-O软件建立文档，怎样引导测试过程，等等。 最重要地，是怎样建造软件使得它一开始就没有错误故障。

 

在软件开发中，可靠性应该是内置的（built-in），而不该是事后回想的（afterthoughts）。

 

参考文献

[1] Bertrand Meyer: Object-Oriented Software Construction , Prentice Hall, 1988. Extensively revised second edition now out.

[2] Bertrand Meyer: Applying "Design by Contract , in Computer (IEEE) , vol. 25, no. 10, October 1992, pages 40-51.

[3] Bertrand Meyer: Eiffel: The Language , Prentice Hall, 1992.

[4] Bertrand Meyer: Systematic Concurrent Object-Oriented Programming , in Communications of the ACM , vol. 36, no. 9, September 1993, pages 56-80.

[5] Kim Waldén and Jean-Marc Nerson, Seamless Object-Oriented Software Architecture: Analysis and Design of Reliable Systems , Prentice Hall, 1995.

注：此文的早期版本发表于Hotline on Object Technology 。

“Design by Contract”是Interactive Software Engineering的商标。

 

---

译后注：

Bertrand Meyer是一位著名的计算机科学家，他的著作“Object-Oriented Software Construction”（OOSC）被称为是O-O技术的经典之作。 Design by Contract “契约式设计”是他对O-O软件开发的重要贡献之一。本文作为一个导引，简明地阐述契约式设计的一些关键 思想和应用。如要详细了解，建议阅读OOSC。

 

此译文中如有所译不当之处，望诸位同行不吝赐教。

 

原文： http://www.eiffel.com/doc/manuals/technology/contract/page.html
2002年1月：译自原文(2002年1月）。