[Python-Dev] Contracts PEP (was re: Introduction)
Terence Way
terry@wayforward.net
Thu, 29 May 2003 14:26:36 -0400
On Wednesday, May 28, 2003, at 06:05 PM, Phillip J. Eby wrote:
> ... I'm still totally not seeing why Alice and Bob have to use the
> same mechanism. Alice could use method wrappers, Bob could use a
> metaclass, and Carol could use assert statements, as far as I can see,
> unless you are looking for static correctness checking. (In which
> case, docstrings are the wrong place for this.)
Here is the full behavior (all quotes are straight from Bertrand
Meyer's Object Oriented Software Construction, 11.1 Inheritance and
Assertions):
"""
Parents' invariant rule: The invariants of all the parents of a class
apply to the class itself.
The parents' invariants are considered to be added to the class's own
invariant, "addition" being here a logical *and*.
"""
Having a single contract implementation means that Bob's overriding
class can check Alice's invariants, even if none of Alice's methods
are actually called.
"""
Assertion redefinition rule: Let r be a routine in class A and s a
redefinition of r in a descendant of A, or an effective definition of
r if r was deferred. Then pre(s) must be weaker than or equal to
pre(r), and post(s) must be stronger than or equal to post(r)
"""
Having a single contract implementation means that Bob's overriding
methods' postconditions check Alice's postconditions, even if none of
Alice's methods are actually called.
I hope I've at least convinced you that it would be nice to have a
single implementation to support 'inv:' and 'post:' with inheritance.
Now on to those irritating pre-conditions.
> That, to me, is weakening a precondition. Now, if what you're saying
> is that Bob's code must work if *Alice's* preconditions are met, then
> that's something different. What you're saying then, is that it's
> required that a precondition in a subclass be logically implied by
> each of the corresponding preconditions in the base classes.
>
> That is certainly a reasonable requirement, but I don't see why the
> language needs to enforce it, certainly not by running Bob's code even
> when Bob's precondition fails! If you're going to enforce it, it
> should be enforced by issuing an error for preconditions that aren't
> logically implied by their superclass preconditions. Then you
> actually get some benefit from the static checking. If you just run
> Bob's code, he has no way to notice that he's violating Alice's
> contract, until his code keeps breaking at runtime. (And then, he
> will almost certainly come to the conclusion that the contract checker
> is broken!)
This is especially irritating because what you're asking for is
exactly what my implementation was doing three weeks ago. I *agree*
with you. There seem to be two opposing groups:
Academics: Pre-conditions are ORed! Liskov Substitution Principle!
Programmers: this is a debugging tool! Tell me when I mess up!
I admit, I'm doing something different by supporting OR pre-
conditions. Meyer again:
"""
So the require and ensure clause must always be given for a routine,
even if it is a redefinition, and even if these clauses are identical
to their antecedents in the original.
"""
Well, this is error-prone and wrong for postconditions. It's not an
issue to just AND a method's post()s with all overridden post()s,
we've covered that earlier. It's only those pesky preconditions.
Summary:
I agree with your point... pre-conditions should only be checked on a
method call for the pre-conditions of the method itself. Overridden
method's preconditions are ignored.
However, this still means some communication between super-class and
overridden class is necessary. Contract invariants and postconditions
conditions of overridden classes/methods still need to be checked.
Cheers!