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

Phillip J. Eby pje@telecommunity.com
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 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.)