What is a type error?

[Darren New]

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.