摘要

本提案描述了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

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

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]，Z模式分为两部分：声明修改内容，然后限制修改。

对 __old__ 值进行变量的浅拷贝可以防止契约编程的实现过多地减慢系统。如果一个函数更改了浅拷贝无法捕获的值，它可以像这样声明更改：

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

在花了一些时间用契约文档化现有函数后，添加了 forall、exists 和 implies 函数。它们捕捉了大多数常见的规范惯用法。定义 implies 为函数可能看起来不起作用（参数无论是否需要都会被求值，与其他布尔运算符不同），但它对契约有效，因为契约中的任何表达式都不应有副作用。

参考实现

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

其他实现方式包括通过修改 __getattr__ [5] 或使用 __metaclass__ [6]。

参考资料

版权

本文档已置于公共领域。