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

[Phillip J. Eby]

At 03:37 PM 5/28/03 -0400, Terence Way wrote:
>On Wednesday, May 28, 2003, at 02:23  PM, Phillip J. Eby wrote:
>>Also, I didn't find the motivation section convincing.  Your answer to 
>>"Why not have several different implementations, or let programmers 
>>implement their own assertions?" isn't actually a justification.  If 
>>Alice uses some package to wrap her methods with checks, I can weaken the 
>>preconditions in a subclass, by simply overriding the methods.  If I 
>>can't do that, then it is a weakness of the DBC package Alice used, or of 
>>Alice's package, not a weakness of Python.
>Consider when Alice's preconditions work, but Bob's do not.  Code that
>thinks it's calling Alice's code *must not* break when calling Bob's.

Okay, you've completely lost me now, because I don't know what you mean by 
"work" in this context.  Do you mean, "are met by the caller"?  Or "are 
syntactically valid"?  Or...?


>Weakening pre-conditions means that Alice's pre-conditions must be
>tested as well: and Bob's code is run even if his pre-conditions fail.

Whaa?  That can't be right.  Weakening a precondition means that Bob's 
preconditions should *replace* Alice's preconditions, if Bob has supplied 
newer, weaker preconditions.  Bob's code should *not* be run if Bob's 
preconditions are not met.

Just to make sure we're not on completely different pages here, I'm 
thinking this:

class AlicesClass:
     def something(self):
         """pre: foo and bar"""

class BobsClass(AlicesClass):
     def something(self):
         """pre: foo"""

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!)

OTOH, if you accept Bob's precondition as he stated it, then he gets the 
behavior he asked for.  If this is a violation of Alice's contract, Bob's 
users will either read the fact in his docs, or complain.


>The converse is also true: code that understands Bob's pre-conditions
>must not fail even if Alice's pre-conditions fail.  This is tough to
>do with asserts, or with incompatible contract packages.

I still don't understand.  If Bob has replaced Alice's method, what do her 
preconditions have to do with it any more?  If Bob's code *calls* Alice's 
method, then the conditions of Alice's method presumably *do* need to apply 
for that upcall, or else she has written them without enough indirection.


>I haven't made that clear in the PEP or the samples, and it needs to
>be clear, because it is the /only/ reason why contracts need to be in
>the language/standard runtime.

Yep, and 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.)