From 613e70e3b898b028bf2afe0e4efbde4cf4cd4308 Mon Sep 17 00:00:00 2001 From: David Goodger Date: Mon, 9 Jun 2003 04:04:03 +0000 Subject: [PATCH] Programming by Contract for Python, by Terence Way --- pep-0316.txt | 418 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 418 insertions(+) create mode 100644 pep-0316.txt diff --git a/pep-0316.txt b/pep-0316.txt new file mode 100644 index 000000000..586b98aa5 --- /dev/null +++ b/pep-0316.txt @@ -0,0 +1,418 @@ +PEP: 316 +Title: Programming by Contract for Python +Version: $Revision$ +Last-Modified: $Date$ +Author: Terence Way +Status: Draft +Type: Standards Track +Content-Type: text/x-rst +Created: 02-May-2003 +Python-Version: +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 pre-conditions under inheritance. + +If Alice produces a class library protected by her own assertions +package, Bob cannot derive classes from Alice's library and weaken the +pre-conditions, unless both have agreed on an assertions system that +supports weakening pre-conditions. 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 + """ + +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 + +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). + +A method's pre-conditions can be ignored if an overridden method's +pre-conditions are met (method pre-conditions are ORed with all +overridden method pre-conditions). This prevents derived classes from +breaking assumptions made by clients that only know the base method's +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__ == 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 are ORed, 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 +========== + +.. [#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://www.python.org/doc/current/lib/module-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/) + +.. [#imp] Implementation described in this document. + (http://www.wayforward.net/pycontract/) + +.. [#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: