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

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!