Abstract

This submission describes programming by contract for Python. Eiffel’s Design By Contract(tm) is perhaps the most popular use of programming contracts [2].

Programming contracts extends the language to include invariant expressions for classes and modules, and pre- and post-condition expressions for functions and methods.

These expressions (contracts) are similar to assertions: they must be true or the program is stopped, and run-time checking of the contracts is typically only enabled while debugging. Contracts are higher-level than straight assertions and are typically included in documentation.

Motivation

Python already has assertions, why add extra stuff to the language to support something like contracts? The two best reasons are 1) better, more accurate documentation, and 2) easier testing.

Complex modules and classes never seem to be documented quite right. The documentation provided may be enough to convince a programmer to use a particular module or class over another, but the programmer almost always has to read the source code when the real debugging starts.

Contracts extend the excellent example provided by the doctest module [4]. Documentation is readable by programmers, yet has executable tests embedded in it.

Testing code with contracts is easier too. Comprehensive contracts are equivalent to unit tests [8]. Tests exercise the full range of pre-conditions, and fail if the post-conditions are triggered. Theoretically, a correctly specified function can be tested completely randomly.

So why add this to the language? Why not have several different implementations, or let programmers implement their own assertions? The answer is the behavior of contracts under inheritance.

Suppose Alice and Bob use different assertions packages. If Alice produces a class library protected by assertions, Bob cannot derive classes from Alice’s library and expect proper checking of post-conditions and invariants. If they both use the same assertions package, then Bob can override Alice’s methods yet still test against Alice’s contract assertions. The natural place to find this assertions system is in the language’s run-time library.

Specification

The docstring of any module or class can include invariant contracts marked off with a line that starts with the keyword inv followed by a colon (:). Whitespace at the start of the line and around the colon is ignored. The colon is either immediately followed by a single expression on the same line, or by a series of expressions on following lines indented past the inv keyword. The normal Python rules about implicit and explicit line continuations are followed here. Any number of invariant contracts can be in a docstring.

Some examples:

# 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)
    """

Module invariants must be true after the module is loaded, and at the entry and exit of every public function within the module.

Class invariants must be true after the __init__ function returns, at the entry of the __del__ function, and at the entry and exit of every other public method of the class. Class invariants must use the self variable to access instance variables.

A method or function is public if its name doesn’t start with an underscore (_), unless it starts and ends with ‘__’ (two underscores).

The docstring of any function or method can have pre-conditions documented with the keyword pre following the same rules above. Post-conditions are documented with the keyword post optionally followed by a list of variables. The variables are in the same scope as the body of the function or method. This list declares the variables that the function/method is allowed to modify.

An example:

class circbuf:

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

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

A double-colon (::) can be used instead of a single colon (:) to support docstrings written using reStructuredText [7]. For example, the following two docstrings describe the same contract:

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

Expressions in pre- and post-conditions are defined in the module namespace – they have access to nearly all the variables that the function can access, except closure variables.

The contract expressions in post-conditions have access to two additional variables: __old__ which is filled with shallow copies of values declared in the variable list immediately following the post keyword, and __return__ which is bound to the return value of the function or method.

An example:

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
        """

All contract expressions have access to some additional convenience functions. To make evaluating the truth of sequences easier, two functions forall and exists are defined as:

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
    """

An example:

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))
    """

To make evaluating conditions easier, the function implies is defined. With two arguments, this is similar to the logical implies (=>) operator. With three arguments, this is similar to C’s conditional expression (x?a:b). This is defined as:

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

On entry to a function, the function’s pre-conditions are checked. An assertion error is raised if any pre-condition is false. If the function is public, then the class or module’s invariants are also checked. Copies of variables declared in the post are saved, the function is called, and if the function exits without raising an exception, the post-conditions are checked.

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)
        """

Rationale

Except for the following differences, programming-by-contract for Python mirrors the Eiffel DBC specification [3].

Embedding contracts in docstrings is patterned after the doctest module. It removes the need for extra syntax, ensures that programs with contracts are backwards-compatible, and no further work is necessary to have the contracts included in the docs.

The keywords pre, post, and inv were chosen instead of the Eiffel-style REQUIRE, ENSURE, and INVARIANT because they’re shorter, more in line with mathematical notation, and for a more subtle reason: the word ‘require’ implies caller responsibilities, while ‘ensure’ implies provider guarantees. Yet pre-conditions can fail through no fault of the caller when using multiple inheritance, and post-conditions can fail through no fault of the function when using multiple threads.

Loop invariants as used in Eiffel are unsupported. They’re a pain to implement, and not part of the documentation anyway.

The variable names __old__ and __return__ were picked to avoid conflicts with the return keyword and to stay consistent with Python naming conventions: they’re public and provided by the Python implementation.

Having variable declarations after a post keyword describes exactly what the function or method is allowed to modify. This removes the need for the NoChange syntax in Eiffel, and makes the implementation of __old__ much easier. It also is more in line with Z schemas [9], which are divided into two parts: declaring what changes followed by limiting the changes.

Shallow copies of variables for the __old__ value prevent an implementation of contract programming from slowing down a system too much. If a function changes values that wouldn’t be caught by a shallow copy, it can declare the changes like so:

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

The forall, exists, and implies functions were added after spending some time documenting existing functions with contracts. These capture a majority of common specification idioms. It might seem that defining implies as a function might not work (the arguments are evaluated whether needed or not, in contrast with other boolean operators), but it works for contracts since there should be no side-effects for any expression in a contract.

Reference Implementation

A reference implementation is available [1]. It replaces existing functions with new functions that do contract checking, by directly changing the class’ or module’s namespace.

Other implementations exist that either hack __getattr__ [5] or use __metaclass__ [6].

References

Copyright

This document has been placed in the public domain.