437 lines
15 KiB
ReStructuredText
437 lines
15 KiB
ReStructuredText
PEP: 316
|
||
Title: Programming by Contract for Python
|
||
Version: $Revision$
|
||
Last-Modified: $Date$
|
||
Author: Terence Way <terry@wayforward.net>
|
||
Status: Deferred
|
||
Type: Standards Track
|
||
Content-Type: text/x-rst
|
||
Created: 02-May-2003
|
||
Post-History:
|
||
|
||
|
||
Abstract
|
||
========
|
||
|
||
This submission describes programming by contract for Python.
|
||
Eiffel's Design By Contract(tm) is perhaps the most popular use of
|
||
programming contracts [#dbc]_.
|
||
|
||
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 [#doctest]_. 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 [#xp]_. 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 [#rst]_. 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.
|
||
|
||
|
||
Exceptions
|
||
----------
|
||
|
||
Class/module invariants are checked even if a function or method exits
|
||
by signalling an exception (post-conditions are not).
|
||
|
||
All failed contracts raise exceptions which are subclasses of the
|
||
``ContractViolationError`` exception, which is in turn a subclass of the
|
||
``AssertionError`` exception. Failed pre-conditions raise a
|
||
``PreconditionViolationError`` exception. Failed post-conditions raise
|
||
a ``PostconditionViolationError`` exception, and failed invariants raise
|
||
a ``InvariantViolationError`` exception.
|
||
|
||
The class hierarchy::
|
||
|
||
AssertionError
|
||
ContractViolationError
|
||
PreconditionViolationError
|
||
PostconditionViolationError
|
||
InvariantViolationError
|
||
InvalidPreconditionError
|
||
|
||
The ``InvalidPreconditionError`` is raised when pre-conditions are
|
||
illegally strengthened, see the next section on Inheritance.
|
||
|
||
Example::
|
||
|
||
try:
|
||
some_func()
|
||
except contract.PreconditionViolationError:
|
||
# failed pre-condition, ok
|
||
pass
|
||
|
||
|
||
Inheritance
|
||
-----------
|
||
|
||
A class's invariants include all the invariants for all super-classes
|
||
(class invariants are ANDed with super-class invariants). These
|
||
invariants are checked in method-resolution order.
|
||
|
||
A method's post-conditions also include all overridden post-conditions
|
||
(method post-conditions are ANDed with all overridden method
|
||
post-conditions).
|
||
|
||
An overridden method's pre-conditions can be ignored if the overriding
|
||
method's pre-conditions are met. However, if the overriding method's
|
||
pre-conditions fail, *all* of the overridden method's pre-conditions
|
||
must also fail. If not, a separate exception is raised, the
|
||
InvalidPreconditionError. This supports weakening pre-conditions.
|
||
|
||
A somewhat contrived example::
|
||
|
||
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)
|
||
"""
|
||
|
||
Because pre-conditions can only be weakened, a ``ComplexMailClient`` can
|
||
replace a ``SimpleMailClient`` with no fear of breaking existing code.
|
||
|
||
|
||
Rationale
|
||
=========
|
||
|
||
Except for the following differences, programming-by-contract for
|
||
Python mirrors the Eiffel DBC specification [#oosc]_.
|
||
|
||
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 [#z]_, 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 [#imp]_. 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__`` [#dbc4p]_
|
||
or use ``__metaclass__`` [#pydbc]_.
|
||
|
||
|
||
References
|
||
==========
|
||
|
||
.. [#imp] Implementation described in this document.
|
||
(http://www.wayforward.net/pycontract/)
|
||
|
||
.. [#dbc] Design By Contract is a registered trademark of Eiffel
|
||
Software Inc.
|
||
(http://archive.eiffel.com/doc/manuals/technology/contract/)
|
||
|
||
.. [#oosc] Object-oriented Software Construction, Bertrand Meyer,
|
||
ISBN 0-13-629031-0
|
||
|
||
.. [#doctest] http://docs.python.org/library/doctest.html
|
||
doctest -- Test docstrings represent reality
|
||
|
||
.. [#dbc4p] Design by Contract for Python, R. Plosch
|
||
*IEEE Proceedings of the Joint Asia Pacific Software Engineering
|
||
Conference (APSEC97/ICSC97), Hong Kong, December 2-5, 1997*
|
||
(http://www.swe.uni-linz.ac.at/publications/abstract/TR-SE-97.24.html)
|
||
|
||
.. [#pydbc] PyDBC -- Design by Contract for Python 2.2+,
|
||
Daniel Arbuckle
|
||
(http://www.nongnu.org/pydbc/)
|
||
|
||
.. [#rst] ReStructuredText (http://docutils.sourceforge.net/rst.html)
|
||
|
||
.. [#xp] Extreme Programming Explained, Kent Beck,
|
||
ISBN 0-201-61641-6
|
||
|
||
.. [#z] The Z Notation, Second Edition, J.M. Spivey
|
||
ISBN 0-13-978529-9
|
||
|
||
|
||
Copyright
|
||
=========
|
||
|
||
This document has been placed in the public domain.
|
||
|
||
|
||
..
|
||
Local Variables:
|
||
mode: indented-text
|
||
indent-tabs-mode: nil
|
||
sentence-end-double-space: t
|
||
fill-column: 70
|
||
End:
|