
I've been lurking for a bit, and now seems like a good time to introduce myself. * I build messaging systems for banks, earlier I was CTO of a dot-com. * I started programming on the TRS-80 and the RCA COSMAC VIP, later on the Apple ][. * I am a Java refugee (well, I might still code in Java for pay). * I'm into formal methods. Translation: I like *talking* about formal methods, but I never use them myself :-) I read somewhere that the best way to build big Python callouses was to write a PEP. Here goes: http://www.wayforward.net/pycontract/pep-0999.html Programming by Contract for Python... pre-conditions, post-conditions, invariants, with all the Eiffel goodness like weakening pre-conditions and strengthening invariants and post-conditions on inheritance, and access to old values. All from docstrings, like doctest. I'm also into handling insane numbers of incoming connections on cheap boxes: compare Jef Poskanzer's thttpd to Apache. 10000 simultaneous HTTP connections on a $400 computer just gets me giggling. Stackless Python intrigues me greatly for the same reason. I guess that's it for now... Cheers!

At 01:32 PM 5/28/03 -0400, Terence Way wrote:
I read somewhere that the best way to build big Python callouses was to write a PEP.
Guess I'll start helping you work on the callouses, then. :)
Here goes: http://www.wayforward.net/pycontract/pep-0999.html
Please don't number a pre-PEP; I believe PEP 1 recomends using 'XXX' until a PEP number has been assigned by the PEP editors.
A number of things aren't clear from your PEP. For example, how would syntax errors in assertions be handled? How is backward compatibility with existing docstrings that may use 'inv:' or 'pre:' to specify conditions informally? Are you proposing that this be part of Python's core syntax? If so, then why do it as docstrings? Are you proposing instead that your implementation be part of the standard library? If so, then where is the documentation for how a developer enables the behavior? 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.

On Wednesday, May 28, 2003, at 02:23 PM, Phillip J. Eby wrote:
Please don't number a pre-PEP; I believe PEP 1 recomends using 'XXX' until a PEP number has been assigned by the PEP editors.
Ack. Oops. I've sent it off to peps@python.org with the XXX, but posted here with the 999.
def read_stuff(input) """pre: input.readline""" would be valid, and the AttributeError would be wrapped inside a PreconditionViolationError if the ``input`` parameter isn't some type of input stream. the core syntax: contracts belong in the documentation, and changing all the doc tools to parse code looking for contract assertions is harder than building one or two docstring implementations. self.note(): where *is* the documentation on how to enable the behavior. thinks it's calling Alice's code *must not* break when calling Bob's. 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. 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 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. Excellent points, thanks for taking an interest.

Hi, I'm Peter. Long time listener, first time caller. On Wed, 28 May 2003, Terence Way wrote:
It seems like either of these methods of coping with legacy docstrings thwart your basic premises. Unless the well-formed nature of the contracts are enforced, it seems to be fairly difficult to e.g. randomly test a function. What if the docstring fails to parse? I have to be listening to stderr to know that it didn't work. I then have to parse the message from stderr to figure out which function didn't work, and finally I have to somehow mark this function as not compliant, and ignore whatever results I get. It really seems like you want them either "on" or "off", not "on, but it might fail in some silent or hard to trap way".
The assertion that contracts don't belong in the core seems entirely seperate from the discussion of their place in docstrings or in real code. That being said, you still haven't explained *why* contracts belong in docstrings (or in documentation in general). They are executable code; why not treat them as such?
self.note(): where *is* the documentation on how to enable the behavior.
I suspect we have to know this before we can know which way is easier. That being said, I really don't see how these contracts can be meaningful as part of a docstring without some better mechanism for handling old docstrings that have been ruled malformed. What's your reasoning against making them their own kind of block, like "try:"? -- Peter

On Wednesday, May 28, 2003, at 04:55 PM, Peter Jones wrote:
I probably would have figured that out too, eventually... :-) More on this further down, when I talk about how to enable docstring testing.
Okay, the whole docstring vs syntax thing, and I'm going to quote liberally from Bertrand Meyer's Object Oriented Software Construction, 1st edition, 7.9 Using Assertions. There are four main reasons for adding contracts to code: """ * Help in writing correct software. * Documentation aid. * Debugging tool. * Support for software fault tolerance. [...] The second use is essential in the production of reusable software elements and, more generally, in organizing the interfaces of modules in large software systems. Preconditions, postconditions, and class invariants provide potential clients of a module with crucial information about the services offered by the module, expressed in a concise and precise form. No amount of verbose documentation can replace a set of carefully expressed assertions. """ I really like Extreme Programming's cut-to-the-bone approach: there are only two things worth knowing about the code: *what* it does and *how* it does it. In XP, what the code does can be inferred from test cases; how it does it from the source code. And if you can't read the code, you have no business talking about how the software does what it does anyway. With contracts, I want to move the knowledge of *what* the code does from the test cases back into the programming documentation. It is merely a bonus feature that this documentation can be executed. When I was learning Python (um, not too long ago) the epiphany of what this language was all about hit me when I saw the 'doctest' module. We're *always* using examples as clear, concise ways to describe what our code does, but we're all guilty of letting those examples get out-of-date. Doctest can crawl into our software deep enough to keep us honest about our documentation. Contracts extend this so it's not just about the basic sample cases, but about the entire state space that a function supports... "Here be dragons" but over there be heap-based priority queues.
Now that I've come out as a doctest fanboy, it should be no surprise that contracts are enabled like this: import contracts, mymodule contracts.checkmod(mymodule) The checkmod side effect is that all functions within mymodule are replaced by auto-generated checking functions. And now I think I'm clear in my own mind about backwards- compatibility with informal 'pre:' docstrings... a programmer doesn't run checkmod unless she's sure that all docstring contracts are valid. Syntax error exceptions will be passed through to the checkmod caller. Cheers!

Terence Way <terry@wayforward.net> writes:
Note: I'm *not* a fan of Eiffel-style formal pre and post conditions. I probably wouldn't use them, personally. But as I could end up dealing with others' code which uses such a feature if it was added, I do have an interest. Also, I haven't read the PEP yet (I'm offline right now). But I disagree fairly strongly with the idea of having pre/post conditions in docstrings. That is *not* what docstrings are for. Docstrings are documentation, not arbitrary metadata. How about this as a proposal? Attach pre and post conditions to a functions as function attributes. A silly example: def f(): pass def pre(): assert True f.pre = pre def post(): assert True f.post = post This is a bit wordy, but entirely doable with Python as it stands and the conditions are syntax checked at definition time, just like they should be. If pre/post conditions turn out to be so useful that they deserve a more concise syntax, *that's* the time to propose better syntax. (One obvious possibility would be to allow more flexibility in def statements, so that def f.post(): whatever becomes possible.) Paul. -- This signature intentionally left blank

On Sunday, June 1, 2003, at 12:17 PM, Paul Moore wrote:
Although I haven't played with it much, in the back of my mind, I think descriptors might be the right implementation technique for this. And the syntax that seems to keep coming up is something like: def f(x, y) [pre, post]: foo() For other reasons, I'm finding that I'd really like to see this syntax for function decorators embodied in its own PEP. -Barry

Barry Warsaw <barry@python.org> writes:
Well, I implemented it, so I've been sort of assuming that I'll be writing the PEP. However if someone else beats me to it, I'm not going to be offended! I'm not going to get to it in a hurry, TBH. Cheers, M. -- Richard Gabriel was wrong: worse is not better, lying is better. Languages and systems succeed in the marketplace to the extent that their proponents lie about what they can do. -- Tim Bradshaw, comp.lang.lisp

On Sun, Jun 01, 2003 at 05:17:10PM +0100, Paul Moore wrote:
FWIW, I stumbled across an implementation of contracts for Python that works more or less in the manner you describe: http://www.nongnu.org/pydbc/ I agree that contracts shouldn't be in docstrings. I confess though, that is because I know editor indenting and syntax highlighting won't handle it smoothly ;) -- Agthorr

FWIW, I stumbled across an implementation of contracts for Python that works more or less in the manner you describe:
With the new surge of interest in metaclasses, I expect many competing DBC implementations to come into existence. An early commitment to one of them may preclude better ideas from getting a chance. Another thought is that all of the machinery is in place to enable a library of cooperating metaclass tools as envisioned by Forman and Danforth's metaclass book. Any metaclass work included in the distribution ought to make allowances for being included side-by-side with threadsafety metaclasses, logging metaclasses, auto property creators, auto delegators, and such. In summary, I prefer that DBC not be PEPed. Instead, let things grow on SF, the cookbook, the vaults, and private offerings. 'nuff said, Raymond Hettinger

Good suggestions! This can be done many ways. Let's find ot which works best. --Guido van Rossum (home page: http://www.python.org/~guido/)

On Sunday, June 1, 2003, at 09:01 PM, Guido van Rossum wrote:
Sigh... PEP withdrawn. I would just like to point out, however, that the challenge with DBC is *not* how to install contracts, whether that's done with meta- classes, attributes, whatever. The challenges are 1) dual use as code and documentation, and 2) correct behavior under inheritance. The problem with multiple implementations is that they may not work together under inheritance, ie all super-class invariants might not be checked, all overridden post-conditions not checked, if the superclass and the derived class use different implementations. What I'll do now is: 1. clean up the loose ends on my implementation; and 2. continue to write contracts for the Python standard library. I've already found 1 bug :-) a full report due soon(ish). Cheers.

At 03:37 PM 5/28/03 -0400, Terence Way wrote:
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.
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.
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.)

On Wednesday, May 28, 2003, at 06:05 PM, Phillip J. Eby wrote:
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.
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!

I think another issue with using doc strings in this way is that you are overloading a feature visible to end users. If I look at the doc string then I would expect to be confused the result:
help(circbuf) Help on class circbuf in module __main__:
class circbuf | Methods defined here: | | get(self) | Pull an entry from a non-empty circular buffer. | | pre: not self.is_empty() | post[self.g, self.len]: | __return__ == self.buf[__old__.self.g] | self.len == __old__.self.len - 1 | ... Way to cryptic even for me :-) I think you could get the same effect by overloading property so you could make methods "smart" about pre and post conditions The following is a first quick hack at it...: class eiffel(property): """eiffel(method,precondition,postcondition) Implement a Eiffel style method that enforces pre- and post- conditions. I guess you could turn this on and off if you wanted... class foo: def pre(self): assert self.x > 0 def post(self): assert self.x > 0 def increment(self): self.x += 1 return increment = eiffel(method,precondition,postcondition) """ def __init__(self,method,precondition,postcondition,doc=None): self.method = method self.precondition = precondition self.postcondition = postcondition super(eiffel,self).__init__(self.__get,None,None,doc) return def __get(self,this): class funny_method: def __init__(self,this,method,precondition,postcondition): self.this = this self.method = method self.precondition = precondition self.postcondition = postcondition return def __call__(self,*args,**kw): self.precondition(self.this) value = self.method(self.this,*args,**kw) self.postcondition(self.this) return value return funny_method(this,self.method,self.precondition,self.postcondition) class circbuf: def __init__(self): self.stack = [] return def _get_pre(self): assert not self.is_empty() return def _get_post(self): assert not self.is_empty() return def _get(self): """Pull an entry from a non-empty circular buffer.""" val = self.stack[-1] del self.stack[-1] return val get = eiffel(_get,_get_pre,_get_post) def put(self,val): self.stack.append(val) return def is_empty(self): return len(self.stack) == 0 B = circbuf() B.put('hello') print B.get() # Will bomb... print B.get() -- Patrick Miller | (925) 423-0309 | http://www.llnl.gov/CASC/people/pmiller If you think you can do a thing or think you can't do a thing, you're right. -- Henry Ford

At 01:32 PM 5/28/03 -0400, Terence Way wrote:
I read somewhere that the best way to build big Python callouses was to write a PEP.
Guess I'll start helping you work on the callouses, then. :)
Here goes: http://www.wayforward.net/pycontract/pep-0999.html
Please don't number a pre-PEP; I believe PEP 1 recomends using 'XXX' until a PEP number has been assigned by the PEP editors.
A number of things aren't clear from your PEP. For example, how would syntax errors in assertions be handled? How is backward compatibility with existing docstrings that may use 'inv:' or 'pre:' to specify conditions informally? Are you proposing that this be part of Python's core syntax? If so, then why do it as docstrings? Are you proposing instead that your implementation be part of the standard library? If so, then where is the documentation for how a developer enables the behavior? 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.

On Wednesday, May 28, 2003, at 02:23 PM, Phillip J. Eby wrote:
Please don't number a pre-PEP; I believe PEP 1 recomends using 'XXX' until a PEP number has been assigned by the PEP editors.
Ack. Oops. I've sent it off to peps@python.org with the XXX, but posted here with the 999.
def read_stuff(input) """pre: input.readline""" would be valid, and the AttributeError would be wrapped inside a PreconditionViolationError if the ``input`` parameter isn't some type of input stream. the core syntax: contracts belong in the documentation, and changing all the doc tools to parse code looking for contract assertions is harder than building one or two docstring implementations. self.note(): where *is* the documentation on how to enable the behavior. thinks it's calling Alice's code *must not* break when calling Bob's. 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. 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 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. Excellent points, thanks for taking an interest.

Hi, I'm Peter. Long time listener, first time caller. On Wed, 28 May 2003, Terence Way wrote:
It seems like either of these methods of coping with legacy docstrings thwart your basic premises. Unless the well-formed nature of the contracts are enforced, it seems to be fairly difficult to e.g. randomly test a function. What if the docstring fails to parse? I have to be listening to stderr to know that it didn't work. I then have to parse the message from stderr to figure out which function didn't work, and finally I have to somehow mark this function as not compliant, and ignore whatever results I get. It really seems like you want them either "on" or "off", not "on, but it might fail in some silent or hard to trap way".
The assertion that contracts don't belong in the core seems entirely seperate from the discussion of their place in docstrings or in real code. That being said, you still haven't explained *why* contracts belong in docstrings (or in documentation in general). They are executable code; why not treat them as such?
self.note(): where *is* the documentation on how to enable the behavior.
I suspect we have to know this before we can know which way is easier. That being said, I really don't see how these contracts can be meaningful as part of a docstring without some better mechanism for handling old docstrings that have been ruled malformed. What's your reasoning against making them their own kind of block, like "try:"? -- Peter

On Wednesday, May 28, 2003, at 04:55 PM, Peter Jones wrote:
I probably would have figured that out too, eventually... :-) More on this further down, when I talk about how to enable docstring testing.
Okay, the whole docstring vs syntax thing, and I'm going to quote liberally from Bertrand Meyer's Object Oriented Software Construction, 1st edition, 7.9 Using Assertions. There are four main reasons for adding contracts to code: """ * Help in writing correct software. * Documentation aid. * Debugging tool. * Support for software fault tolerance. [...] The second use is essential in the production of reusable software elements and, more generally, in organizing the interfaces of modules in large software systems. Preconditions, postconditions, and class invariants provide potential clients of a module with crucial information about the services offered by the module, expressed in a concise and precise form. No amount of verbose documentation can replace a set of carefully expressed assertions. """ I really like Extreme Programming's cut-to-the-bone approach: there are only two things worth knowing about the code: *what* it does and *how* it does it. In XP, what the code does can be inferred from test cases; how it does it from the source code. And if you can't read the code, you have no business talking about how the software does what it does anyway. With contracts, I want to move the knowledge of *what* the code does from the test cases back into the programming documentation. It is merely a bonus feature that this documentation can be executed. When I was learning Python (um, not too long ago) the epiphany of what this language was all about hit me when I saw the 'doctest' module. We're *always* using examples as clear, concise ways to describe what our code does, but we're all guilty of letting those examples get out-of-date. Doctest can crawl into our software deep enough to keep us honest about our documentation. Contracts extend this so it's not just about the basic sample cases, but about the entire state space that a function supports... "Here be dragons" but over there be heap-based priority queues.
Now that I've come out as a doctest fanboy, it should be no surprise that contracts are enabled like this: import contracts, mymodule contracts.checkmod(mymodule) The checkmod side effect is that all functions within mymodule are replaced by auto-generated checking functions. And now I think I'm clear in my own mind about backwards- compatibility with informal 'pre:' docstrings... a programmer doesn't run checkmod unless she's sure that all docstring contracts are valid. Syntax error exceptions will be passed through to the checkmod caller. Cheers!

Terence Way <terry@wayforward.net> writes:
Note: I'm *not* a fan of Eiffel-style formal pre and post conditions. I probably wouldn't use them, personally. But as I could end up dealing with others' code which uses such a feature if it was added, I do have an interest. Also, I haven't read the PEP yet (I'm offline right now). But I disagree fairly strongly with the idea of having pre/post conditions in docstrings. That is *not* what docstrings are for. Docstrings are documentation, not arbitrary metadata. How about this as a proposal? Attach pre and post conditions to a functions as function attributes. A silly example: def f(): pass def pre(): assert True f.pre = pre def post(): assert True f.post = post This is a bit wordy, but entirely doable with Python as it stands and the conditions are syntax checked at definition time, just like they should be. If pre/post conditions turn out to be so useful that they deserve a more concise syntax, *that's* the time to propose better syntax. (One obvious possibility would be to allow more flexibility in def statements, so that def f.post(): whatever becomes possible.) Paul. -- This signature intentionally left blank

On Sunday, June 1, 2003, at 12:17 PM, Paul Moore wrote:
Although I haven't played with it much, in the back of my mind, I think descriptors might be the right implementation technique for this. And the syntax that seems to keep coming up is something like: def f(x, y) [pre, post]: foo() For other reasons, I'm finding that I'd really like to see this syntax for function decorators embodied in its own PEP. -Barry

Barry Warsaw <barry@python.org> writes:
Well, I implemented it, so I've been sort of assuming that I'll be writing the PEP. However if someone else beats me to it, I'm not going to be offended! I'm not going to get to it in a hurry, TBH. Cheers, M. -- Richard Gabriel was wrong: worse is not better, lying is better. Languages and systems succeed in the marketplace to the extent that their proponents lie about what they can do. -- Tim Bradshaw, comp.lang.lisp

On Sun, Jun 01, 2003 at 05:17:10PM +0100, Paul Moore wrote:
FWIW, I stumbled across an implementation of contracts for Python that works more or less in the manner you describe: http://www.nongnu.org/pydbc/ I agree that contracts shouldn't be in docstrings. I confess though, that is because I know editor indenting and syntax highlighting won't handle it smoothly ;) -- Agthorr

FWIW, I stumbled across an implementation of contracts for Python that works more or less in the manner you describe:
With the new surge of interest in metaclasses, I expect many competing DBC implementations to come into existence. An early commitment to one of them may preclude better ideas from getting a chance. Another thought is that all of the machinery is in place to enable a library of cooperating metaclass tools as envisioned by Forman and Danforth's metaclass book. Any metaclass work included in the distribution ought to make allowances for being included side-by-side with threadsafety metaclasses, logging metaclasses, auto property creators, auto delegators, and such. In summary, I prefer that DBC not be PEPed. Instead, let things grow on SF, the cookbook, the vaults, and private offerings. 'nuff said, Raymond Hettinger

Good suggestions! This can be done many ways. Let's find ot which works best. --Guido van Rossum (home page: http://www.python.org/~guido/)

On Sunday, June 1, 2003, at 09:01 PM, Guido van Rossum wrote:
Sigh... PEP withdrawn. I would just like to point out, however, that the challenge with DBC is *not* how to install contracts, whether that's done with meta- classes, attributes, whatever. The challenges are 1) dual use as code and documentation, and 2) correct behavior under inheritance. The problem with multiple implementations is that they may not work together under inheritance, ie all super-class invariants might not be checked, all overridden post-conditions not checked, if the superclass and the derived class use different implementations. What I'll do now is: 1. clean up the loose ends on my implementation; and 2. continue to write contracts for the Python standard library. I've already found 1 bug :-) a full report due soon(ish). Cheers.

At 03:37 PM 5/28/03 -0400, Terence Way wrote:
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.
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.
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.)

On Wednesday, May 28, 2003, at 06:05 PM, Phillip J. Eby wrote:
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.
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!

I think another issue with using doc strings in this way is that you are overloading a feature visible to end users. If I look at the doc string then I would expect to be confused the result:
help(circbuf) Help on class circbuf in module __main__:
class circbuf | Methods defined here: | | get(self) | Pull an entry from a non-empty circular buffer. | | pre: not self.is_empty() | post[self.g, self.len]: | __return__ == self.buf[__old__.self.g] | self.len == __old__.self.len - 1 | ... Way to cryptic even for me :-) I think you could get the same effect by overloading property so you could make methods "smart" about pre and post conditions The following is a first quick hack at it...: class eiffel(property): """eiffel(method,precondition,postcondition) Implement a Eiffel style method that enforces pre- and post- conditions. I guess you could turn this on and off if you wanted... class foo: def pre(self): assert self.x > 0 def post(self): assert self.x > 0 def increment(self): self.x += 1 return increment = eiffel(method,precondition,postcondition) """ def __init__(self,method,precondition,postcondition,doc=None): self.method = method self.precondition = precondition self.postcondition = postcondition super(eiffel,self).__init__(self.__get,None,None,doc) return def __get(self,this): class funny_method: def __init__(self,this,method,precondition,postcondition): self.this = this self.method = method self.precondition = precondition self.postcondition = postcondition return def __call__(self,*args,**kw): self.precondition(self.this) value = self.method(self.this,*args,**kw) self.postcondition(self.this) return value return funny_method(this,self.method,self.precondition,self.postcondition) class circbuf: def __init__(self): self.stack = [] return def _get_pre(self): assert not self.is_empty() return def _get_post(self): assert not self.is_empty() return def _get(self): """Pull an entry from a non-empty circular buffer.""" val = self.stack[-1] del self.stack[-1] return val get = eiffel(_get,_get_pre,_get_post) def put(self,val): self.stack.append(val) return def is_empty(self): return len(self.stack) == 0 B = circbuf() B.put('hello') print B.get() # Will bomb... print B.get() -- Patrick Miller | (925) 423-0309 | http://www.llnl.gov/CASC/people/pmiller If you think you can do a thing or think you can't do a thing, you're right. -- Henry Ford
participants (10)
-
Agthorr
-
Barry Warsaw
-
Guido van Rossum
-
Michael Hudson
-
Pat Miller
-
Paul Moore
-
Peter Jones
-
Phillip J. Eby
-
Raymond Hettinger
-
Terence Way