ANN: Design By Contract for Python 1.0 beta 1

[Terence Way]

On Mon, 26 May 2003 13:56:07 -0400, Jeff Epler wrote:

> Is there a reason that you don't use exception subclasses to
> differentiate between different kinds of contract failures?  The
> hierarchy might look like
> 	ContractViolationError
> 		PreconditionViolationError
> 		PostconditionViolationError
> 		ClassInvariantViolationError
> 
> I glanced at the Eiffel page you linked form the PEP and they had some
> form of error recovery capability.  Did you address why you decided not
> to include this in your PEP?

Um, no.  Oops.  This makes the sample code I included that differentiates
based on Exception argument look dumb.  Just plain laziness on my part,
for a pre-condition 'pre: x > 0' my code just does a
'assert x > 0, "pre"'

I will take your suggestion verbatim, if you don't mind, except that
ClassInvariantViolationError will be replaced by InvariantViolationError,
cuz modules can have invariants, too.  Also ContractViolationError will
inherit from AssertionError.

> If your feature could be adopted either in the form of a
> specially-formatted docstring or as actual "code", which would you
> prefer? Typically, editors will decline to do syntax highlighting or
> automatic indentation of string contents.

I'm having this discussion with a couple other people...  actual code
has the advantage of access to closure variables... docstrings has the
advantage of, um, well, keeping the contracts in the documentation.

At least two possible ways of handling this...  referring to a function
in the docstring:
     def foo(a, b):
         """pre: foo_pre(a, b)"""

     def foo_pre(a, b)

Or, among all the approaches to 'installing' pre-conditions, post-
conditions, etc. the one I like best is function attributes:

    def foo(a, b):
        pass
    def foo_pre(a, b):
        ...
    foo.__pre__ = foo_pre

Pre-conditions are easy, but post-conditions are hard.  There needs to
be *two* separate functions, one to save 'old' values, and one to test
for actual post-conditions.  I imagine there are going to be a few cases
where the docstring conventions just don't work... access to closure
variables is one case that I know about already.

Perhaps there are three reserved attributes for functions:  __pre__,
__old__, and __post__.  If set, they must point to functions
that assert pre-conditions, save old variables, and assert post-
conditions, respectively.  Any expressions in the docstring will
override any attribute-based contracts.  Modules and classes have
an '__inv__' attribute, similarly.

> Why do you use "inv:" instead of "invariant:"?  The only exceptions to
> the "english word" rule in Python's existing reserved words are "def",
> "del" and "elif". (Of course, 3 exceptions out of 29 is quite a few) For
> whatever reason, I don't feel as weird about "pre:" and "post:" as I do
> about "inv:".

Agreed.  'require' and 'ensure' just don't feel Pythonic to me, and
the 'pre' and 'post' feel right.  The *primary* reason I chose 'inv' is:
I originally had 'require' 'ensure' and 'invariant' but then I started
writing code using 'requires' 'ensures' and 'invariants.'  It turns out
in my current implementation to be kinda hard to tell if a running program
has the correct contracts installed.  It took me a while to figure out why
my code wasn't breaking where I expected it to.  I don't want to support
more than one keyword... so I thought using the abbreviations would
make it clear that plurals aren't welcome.

> Does Eiffel have a syntax for *loop* invariants? eg
> 	def index_of_largest(l):
> 		largest = l[0]
> 		for i in range(1, len(l)):
> 			invariant: forall(range(i), lambda x: largest >= l[x]) if l[i] >
> 			largest: largest = l[i]

Yes, Eiffel does have loop invariants... and there are people that swear
by them.  One cool thing you can do with loop invariants is write
programs that can provably complete, short-circuiting the Turing
completion problem.  Cool.  And completely out of the scope of what I'm
trying to do.  I think adding loop invariants would mean changes to the
core language.


> Jeff