[Python-ideas] Pre-conditions and post-conditions
Marko Ristin-Kaufmann
marko.ristin at gmail.com
Sat Aug 25 04:04:45 EDT 2018
Hi,
@Paul Moore: thanks for pointing out that many people are not familiar with
design-by-contract. I was not aware of that.
Let me give you a very short introduction into contracts and what they are
good for. I'll review some existing libraries and highlight what features
we missed (and why we developed our own library). I will finally conclude
with why all these solutions (including our own one) are not a replacement
for a proper support of design-by-contract in the language.
Design-by-Contract
Design-by-contract was gradually introduced as a concept by Bertrand Meyer
in the 1980ies to provide a formal and verifiable interface specification
between the software components. Up to then the interfaces were usually
defined formally in terms of abstract data types (think of records /
structs and classes). He extended abstract data types by adding "contract"
conditions that should hold at different points during the execution of a
program. The contracts allow you to formally write down your expectations
about the program (as opposed to writing it informally in documentation of
a class or a function). Hence we can automatically test that they hold
either statically or during the execution of the program. This gives us
many-fold benefits:
- contracts prevent code rot (since they can be checked by a compiler or
a static analysis tool such as mypy),
- allow us to have much more sophisticated automatic generation of unit
tests and automatic formal proofs of a program,
- make the documentation explicit, accurate and verifiable and
- accelerate the development since errors are caught early.
The contracts are categorized as follows depending on at which point in the
program they are verified:
- Preconditions are contracts that should hold before the execution of a
function. The *caller* is responsible to fulfill the preconditions.
- Postconditions are contracts that should hold after the execution of a
function. The *callee* is responsible to fulfill the postconditions.
- Invariants should hold throughout the execution of the program. There
are two types of invariants: loop invariants and class invariants.
- Loop invariants should hold before and after each iteration step of a
loop.
- Class invariants should hold throughout the life time of a class (
*i.e.* between the calls to the public methods). The class invariants
are suspended during the construction of an instance and in private methods
to avoid cycles. You can think of the constructor method and public methods
being responsible to fulfill the class invariants.
The concept of design-by-contract is not limited only to concrete classes,
but can be also applied to class hierarchies. Preconditions, postconditions
and invariants are inherited. They can be also modified in the following
ways:
- The child class needs to fulfill all the invariants of its antecedent
classes and its own ones.
- The preconditions of a function of a child class can "weaken" or
"relax" the preconditions of the parent class. In other words, it needs to
fulfill *either* the preconditions of the parent class *or *its own set
of preconditions. This is reflected in Eiffel by using the keyword *require
else.*
- The postconditions of a a child class can "strengthen" or "tighten"
the postconditions of the parent class. The function needs to fulfill all
the postconditions of the parent class' function *and *its own set of
postconditions. In Eiffel, this is designated with *ensure then* keyword.
Invariants operate only on the values of instance properties. Preconditions
operate on both function arguments and instance properties. Postconditions
need yet one more instrument: they operate on function arguments, instance
properties and the result of a function, but can access all these values
both at their *old* state, before the function call, and their *new *state,
after the function call. In Eiffel, you use the keyword *old* to indicate
the value before the function call.
Let me illustrate the concepts by adapting the examples from
https://www.eiffel.org/doc/eiffel/ET-_Design_by_Contract_%28tm%29%2C_Assertions_and_Exceptions
and https://www.eiffel.org/doc/eiffel/ET-_Inheritance. I will paraphrase
the example code in Python assuming that invariant, require, ensure and old
were introduced as keywords.
*class *Account:
*def *__init__(self, balance: int) -> *None*:
self.balance = balance
self.deposits = [] *# type: List[int]
**def *update(self, sum: int)->*None*:
require: sum >= 0
self.balance += sum
self.deposits.append(sum)
ensure: len(self.deposits) = len(old self.deposits) + 1, *"one
more deposit"
*ensure: self.balance = old self.balance + sum, *"updated"
*invariant: *not *self.deposits *or *self.balance ==
sum(self.deposits), *"consistent balance"
*invariant: self.deposits *or *self.balance == 0, *"zero if no deposits"
class *CheckingAccount(Account):
*def *update(self, sum: int) -> *None*:
require *else*: self.balance >= sum
self.balance += sum
self.deposits.append(sum)
invariant: self.balance >= 0
For more examples and details, please see the before-mentioned two web
pages on Eiffel.
Current Implementations
A series of open-sourced libraries have been developed to bring
design-by-contract to Python.
*PyContracts* (https://pypi.org/project/PyContracts/) introduced the
preconditions and postconditions as special annotations:
@contract
def my_function(a : 'int,>0', b : 'list[N],N>0') -> 'list[N]':
# Requires b to be a nonempty list, and the return
# value to have the same length.
...
new_contract('valid_name', lambda s: isinstance(s, str) and len(s)>0)
@contract(names='dict(int: (valid_name, int))')
def process_accounting(records):
...
I personally find these annotations hard to read. The contracts seem mostly
focused on type checks and on single arguments. Moreover, without support
in IDEs and static analysis tools, annotations are susceptible to code rot
if not verified by a linter (as far as I could find out, there are not
linters that check pycontracts -- please correct me if I'm wrong). I also
don't see how you could elegantly implement a check based on multiple
arguments (*e.g., *sum >= balance in the CheckingAccount example).
*Dpcontracts* (https://pypi.org/project/dpcontracts/) is a library based on
decorators. It encapsulates the arguments of a function and its result as
the arguments of the condition function:
>>> @require("`i` must be a positive integer",
... lambda args: isinstance(args.i, int) and args.i > 0)
... @require("`j` must be a positive integer",
... lambda args: isinstance(args.j, int) and args.j > 0)
... @ensure("the result must be greater than either `i` or `j`",
... lambda args, result: result > args.i and result > args.j)
... def add2(i, j):
... if i == 7:
... i = -7 # intentionally broken for purposes of example
... return i + j
It also supports invariants:
>>> @invariant("inner list can never be empty", lambda self: len(self.lst) > 0)
... @invariant("inner list must consist only of integers",
... lambda self: all(isinstance(x, int) for x in self.lst))
... class NonemptyList:
... @require("initial list must be a list", lambda args:
isinstance(args.initial, list))
... @require("initial list cannot be empty", lambda args:
len(args.initial) > 0)
... @ensure("the list instance variable is equal to the given argument",
... lambda args, result: args.self.lst == args.initial)
... @ensure("the list instance variable is not an alias to the
given argument",
... lambda args, result: args.self.lst is not args.initial)
... def __init__(self, initial):
... self.lst = initial[:]
...
... def get(self, i):
... return self.lst[i]
...
... def pop(self):
... self.lst.pop()
...
... def as_string(self):
... # Build up a string representation using the `get` method,
... # to illustrate methods calling methods with invariants.
... return ",".join(str(self.get(i)) for i in range(0, len(self.lst)))
Contracts (https://pypi.org/project/contracts/), pyadbc (
https://pypi.org/project/pyadbc/) and pcd (https://pypi.org/project/pcd/)
are similar in terms of features to dpcontracts, but seem not to be
maintained any more.
We found that all the presented methods were a bit impractical to use in
everyday programming. Pycontracts forces the programmer to learn a new
syntax which is not statically checked. While we liked the features
provided by dpcontracts, we found that exception messages thrown at
contract breach were uninformative. The programmer is forced to repeat
every condition in text if s/he is to make any use of the error once it
happens. This can lead to mismatch between the messages and code (similar
how the comments tend to rot) and can make debugging and tracing bugs very
hard. Moreover, it is tedious and repetitive to document the conditions
twice which makes programmers sometimes reluctant to adopt it and apply it
widely.
We therefore developed *icontract* (https://pypi.org/project/icontract/).
We decided to leave out class invariants for practical reasons (we rarely
use classes in our applications and we needed conditions in production for
which the invariants are often impractical), but invariants can be easily
added if there is a demand. icontract is based on decorators and uses
lambda functions for the conditions that match the argument names of the
function. The argument *result* is reserved for the result of the function
in postconditions. Here is the example usage:
>>> @icontract.pre(lambda x: x > 3)... def some_func(x: int, y: int = 5)->None:... pass...
>>> some_func(x=5)
# Pre-condition violation>>> some_func(x=1)Traceback (most recent call last):
...icontract.ViolationError: Precondition violated: x > 3: x was 1
>>> @icontract.post(lambda result, x: result > x)... def some_func(x: int, y: int = 5) -> int:... return x - y...>>> some_func(x=10)Traceback (most recent call last):
...icontract.ViolationError: Post-condition violated: result >
x:result was 5x was 10
Mind that there is no mandatory description in the contract yet the message
is informative. We achieve that by re-executing the condition function and
tracing the values by examining its abstract syntax tree. The
re-computation can also deal with more complex expressions and outer scope:
>>> class B:... def __init__(self) -> None:... self.x = 7...... def y(self) -> int:... return 2...... def __repr__(self) -> str:... return "instance of B"...>>> class A:... def __init__(self)->None:... self.b = B()...... def __repr__(self) -> str:... return "instance of A"...>>> SOME_GLOBAL_VAR = 13>>> @icontract.pre(lambda a: a.b.x + a.b.y() > SOME_GLOBAL_VAR)... def some_func(a: A) -> None:... pass...>>> an_a = A()>>> some_func(an_a)Traceback (most recent call last):
...icontract.ViolationError: Precondition violated: (a.b.x +
a.b.y()) > SOME_GLOBAL_VAR:SOME_GLOBAL_VAR was 13a was instance of
Aa.b was instance of Ba.b.x was 7a.b.y() was 2
We found informative messages to be a tremendous booster when debugging
since you often immediately see what caused the contract breach and not
only that it was broken. This often points you directly to the cause of the
bug.
Moreover, conditions are much more readable when not cluttered by redundant
descriptions. This is important when you use them as part of the
documentation that you inspect with an IDE (*e.g., *in PyCharm). By our
subjective impression, other solutions resulted in hard-to-read
documentation in PyCharm. While descriptions can also be added to the
icontract conditions, we rarely find that necessary since most conditions
are self-explanatory.
Insufficiencies of the Current Libraries
All the libraries described here were not trivial to implement and come
with a substantial computational overhead. In one of our benchmarks, we
found that having a precondition made a function run at least 6x slower (we
traced the slow-down to an additional function invocation which is costly
in Python). I don't think that it is possible to implement *old *keyword
for most practical applications since the execution would be even slower.
I found no library so far that supports inheritance, strengthening (ensure
then) and weakening (*require else)* of the contracts out-of-the-box. My
intuition tells me that it is possible to implement such a feature in a
library, but the implementation will definitely be very complex.
Apart from computational efficiency and complexity of implementation, I
also see the variety of libraries as a problem for the adoption of
design-by-contract. With multiple solutions and each team having their own
preferences there is a dilemma which solution to choose. Without a wide
adoption of a single solution we can not expect an emergence of tools such
as automatic test generators built on top of the contracts which is where
the actual tremendous benefits really await.
A standard solution would allow us to have uniform, widely-adopted and
efficient design-by-contracts in Python which no library by itself can
achieve.
Sketch of a Solution
Instead of introducing new keywords, Python could introduce a built-in
module based on decorators. The interpreters could be extended such as that
they in-line the code directly into the function whenever the decorators of
this built-in module is encountered. This would substantially reduce the
computational overhead while it would allow us to avoid changes to language
syntax.
However, before we even start looking at a solution, I see it necessary
that we first discuss more to which degree contracts should be introduced
to Python and what the use cases would look like.
Cheers,
Marko
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-ideas/attachments/20180825/e9b4b3d2/attachment-0001.html>
More information about the Python-ideas
mailing list