[Python-Dev] Contracts PEP (was re: Introduction)
Phillip J. Eby
Wed, 28 May 2003 18:05:30 -0400
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
"""pre: foo and bar"""
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.)