[Python-Dev] Contracts PEP (was re: Introduction)

[Terence Way]

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!