摘要

本提交描述了 Python 的契约式编程。Eiffel 的 Design By Contract(tm) 可能是契约式编程最流行的应用 [2]。

契约式编程扩展了语言，为类和模块包含了不变式表达式，以及为函数和方法包含了前置条件和后置条件表达式。

这些表达式（契约）类似于断言：它们必须为真，否则程序将停止，并且在调试时通常只启用契约的运行时检查。契约比简单的断言更高级别，通常包含在文档中。

动机

Python 已经有了断言，为什么还要向语言中添加额外的东西来支持像契约这样的东西？两个最主要的原因是 1) 更好、更准确的文档，以及 2) 更简单的测试。

复杂模块和类似乎永远无法得到完全正确的文档。提供的文档可能足以说服程序员选择使用某个特定的模块或类，但当真正的调试开始时，程序员几乎总是必须阅读源代码。

契约扩展了 doctest 模块提供的优秀示例 [4]。文档可以被程序员阅读，并且在其中嵌入了可执行的测试。

使用契约测试代码也更容易。全面的契约等同于单元测试 [8]。测试涵盖了所有前置条件，如果触发后置条件则会失败。理论上，可以完全随机地测试正确指定的函数。

那么为什么将其添加到语言中呢？为什么不使用几种不同的实现，或者让程序员实现自己的断言呢？答案在于继承下的契约行为。

假设 Alice 和 Bob 使用不同的断言包。如果 Alice 创建了一个受断言保护的类库，Bob 无法从 Alice 的库派生类并期望正确检查后置条件和不变式。如果他们都使用相同的断言包，那么 Bob 可以覆盖 Alice 的方法，但仍然可以针对 Alice 的契约断言进行测试。在语言的运行时库中自然可以找到这个断言系统。

规范

任何模块或类的文档字符串都可以包含用以 inv 关键字开头的行标记的不变式契约（后跟冒号(:)）。行首和冒号周围的空格将被忽略。冒号后面紧跟着同一行上的单个表达式，或者后面跟着以下几行中缩进到 inv 关键字之后的表达式序列。此处遵循关于隐式和显式换行的正常 Python 规则。文档字符串中可以包含任意数量的不变式契约。

一些例子

# state enumeration
START, CONNECTING, CONNECTED, CLOSING, CLOSED = range(5)

class conn:

    """A network connection

    inv: self.state in [START, CLOSED,       # closed states
                        CONNECTING, CLOSING, # transition states
                        CONNECTED]

    inv: 0 <= self.seqno < 256
    """

class circbuf:

    """A circular buffer.

    inv:
        # there can be from 0 to max items on the buffer
        0 <= self.len <= len(self.buf)

        # g is a valid index into buf
        0 <= self.g < len(self.buf)

        # p is also a valid index into buf
        0 <= self.p < len(self.buf)

        # there are len items between get and put
        (self.p - self.g) % len(self.buf) == \
              self.len % len(self.buf)
    """

模块不变式必须在模块加载后、每个公共函数进入和退出时都为真。

类不变式必须在 __init__ 函数返回后、在 __del__ 函数进入时，以及在类的每个其他公共方法进入和退出时都为真。类不变式必须使用 self 变量来访问实例变量。

如果方法或函数的名称不以下划线 (_) 开头，则该方法或函数为公共方法或函数，除非它以两个下划线 ('__') 开头和结尾。

任何函数或方法的文档字符串都可以使用 pre 关键字记录前置条件，遵循上述相同的规则。后置条件使用 post 关键字记录，后面可以选择跟一个变量列表。这些变量与函数或方法的正文位于相同的范围内。此列表声明了函数/方法允许修改的变量。

一个例子

class circbuf:

    def __init__(self, leng):
        """Construct an empty circular buffer.

        pre: leng > 0
        post[self]:
            self.is_empty()
            len(self.buf) == leng
        """

可以使用双冒号 (::) 代替单冒号 (:) 来支持使用 reStructuredText 编写的文档字符串 [7]。例如，以下两个文档字符串描述了相同的契约

"""pre: leng > 0"""
"""pre:: leng > 0"""

前置条件和后置条件中的表达式在模块命名空间中定义 - 它们可以访问函数几乎可以访问的所有变量，除了闭包变量。

后置条件中的契约表达式可以访问两个额外的变量：__old__，它填充了紧跟在 post 关键字后面的变量列表中声明的值的浅拷贝，以及 __return__，它绑定到函数或方法的返回值。

一个例子

class circbuf:

    def get(self):
        """Pull an entry from a non-empty circular buffer.

        pre: not self.is_empty()
        post[self.g, self.len]:
            __return__ == self.buf[__old__.self.g]
            self.len == __old__.self.len - 1
        """

所有契约表达式都可以访问一些额外的便捷函数。为了更容易评估序列的真值，定义了两个函数 forall 和 exists，如下所示

def forall(a, fn = bool):
    """Return True only if all elements in a are true.

    >>> forall([])
    1
    >>> even = lambda x: x % 2 == 0
    >>> forall([2, 4, 6, 8], even)
    1
    >>> forall('this is a test'.split(), lambda x: len(x) == 4)
    0
    """

def exists(a, fn = bool):
    """Returns True if there is at least one true value in a.

    >>> exists([])
    0
    >>> exists('this is a test'.split(), lambda x: len(x) == 4)
    1
    """

一个例子

def sort(a):
    """Sort a list.

    pre: isinstance(a, type(list))
    post[a]:
        # array size is unchanged
        len(a) == len(__old__.a)

        # array is ordered
        forall([a[i] >= a[i-1] for i in range(1, len(a))])

        # all the old elements are still in the array
        forall(__old__.a, lambda e: __old__.a.count(e) == a.count(e))
    """

为了更容易评估条件，定义了函数 implies。有两个参数时，它类似于逻辑蕴含 (=>) 运算符。有三个参数时，它类似于 C 的条件表达式 (x?a:b)。它定义如下

implies(False, a) => True
implies(True, a) => a
implies(False, a, b) => b
implies(True, a, b) => a

在进入函数时，将检查函数的前置条件。如果任何前置条件为假，则会引发断言错误。如果函数是公共函数，则还会检查类或模块的不变式。保存 post 中声明的变量的副本，调用函数，如果函数退出时未引发异常，则检查后置条件。

AssertionError
    ContractViolationError
        PreconditionViolationError
        PostconditionViolationError
        InvariantViolationError
        InvalidPreconditionError

try:
    some_func()
except contract.PreconditionViolationError:
    # failed pre-condition, ok
    pass

class SimpleMailClient:

    def send(self, msg, dest):
        """Sends a message to a destination:

        pre: self.is_open() # we must have an open connection
        """

    def recv(self):
        """Gets the next unread mail message.

        Returns None if no message is available.

        pre: self.is_open() # we must have an open connection
        post: __return__ is None or isinstance(__return__, Message)
        """

 class ComplexMailClient(SimpleMailClient):
    def send(self, msg, dest):
        """Sends a message to a destination.

        The message is sent immediately if currently connected.
        Otherwise, the message is queued locally until a
        connection is made.

        pre: True # weakens the pre-condition from SimpleMailClient
        """

    def recv(self):
        """Gets the next unread mail message.

        Waits until a message is available.

        pre: True # can always be called
        post: isinstance(__return__, Message)
        """

基本原理

除了以下差异外，Python 的契约式编程与 Eiffel DBC 规范类似 [3]。

将契约嵌入到文档字符串中是根据 doctest 模块设计的。它消除了对额外语法的需求，确保带有契约的程序向后兼容，并且无需进一步的工作即可将契约包含在文档中。

选择关键字 pre、post 和 inv 而不是 Eiffel 风格的 REQUIRE、ENSURE 和 INVARIANT，因为它们更短，更符合数学符号，并且还有一个更微妙的原因：单词“require”暗示调用者的责任，而“ensure”暗示提供者的保证。然而，在使用多重继承时，前置条件可能会因调用者之外的原因而失败，在使用多线程时，后置条件可能会因函数之外的原因而失败。

不支持 Eiffel 中使用的循环不变式。它们难以实现，并且无论如何都不是文档的一部分。

选择变量名 __old__ 和 __return__ 以避免与 return 关键字冲突，并保持与 Python 命名约定的 一致性：它们是公共的，由 Python 实现提供。

在 post 关键字之后声明变量准确地描述了函数或方法允许修改的内容。这消除了对 Eiffel 中 NoChange 语法的需求，并且使 __old__ 的实现变得更加容易。它也更符合 Z 模式 [9]，后者分为两部分：声明更改的内容，然后限制更改的内容。

为 __old__ 值创建变量的浅拷贝可以防止契约编程的实现过度降低系统速度。如果函数更改了不会被浅拷贝捕获的值，它可以像这样声明更改

post[self, self.obj, self.obj.p]

在花费一些时间使用契约记录现有函数后，添加了 forall、exists 和 implies 函数。这些函数涵盖了大多数常见的规范习惯用法。似乎将 implies 定义为函数可能不起作用（无论是否需要都会评估参数，这与其他布尔运算符形成对比），但它对契约有效，因为契约中的任何表达式都不应有副作用。

参考实现

参考实现可用 [1]。它通过直接更改类或模块的命名空间，用执行契约检查的新函数替换现有函数。

其他实现也存在，它们要么修改 __getattr__ [5]，要么使用 __metaclass__ [6]。

参考文献

版权

本文档已进入公有领域。