Marshall wrote:
> Now, I'm not fully up to speed on DBC. The contract specifications,
> these are specified statically, but checked dynamically, is that
> right?
Yes, but there's a bunch more to it than that. The handling of
exceptions, an in particular exceptions caused by failed pre/post
conditions, is an integral part of the process.
Plus, of course, pre/post condition checking is turned off while
checking pre/post conditions. This does make sense if you think about it
long enough, but it took me several months before I realized why it's
necessary theoretically rather than just practically.
> Wouldn't it be possible to do them at compile time?
For some particularly simple ones, yes. For others, like "the chess
pieces are in a position it is legal to get to from a standard opening
set-up", it would be difficult. Anything to do with I/O is going to be
almost impossible to write a checkable postcondition for, even at
runtime. "After this call, the reader at the other end of the socket
will receive the bytes in argument 2 without change."
As far as I understand it, Eiffel compilers don't even make use of
postconditions to optimize code or eliminate run-time checks (like null
pointer testing).
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
--
http://mail.python.org/mailman/listinfo/python-list
