python-peps / pep-0316.txt

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
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
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 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__ == 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:
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.