What is a type error?

[David Hopwood]

Marshall wrote:
> Joachim Durchholz wrote:
[...]
>>Preconditions/postconditions can express anything you want, and they are
>>an absolutely natural extensions of what's commonly called a type
>>(actually the more powerful type systems have quite a broad overlap with
>>assertions).
>>I'd essentially want to have an assertion language, with primitives for
>>type expressions.
> 
> Now, I'm not fully up to speed on DBC. The contract specifications,
> these are specified statically, but checked dynamically, is that
> right? In other words, we can consider contracts in light of
> inheritance, but the actual verification and checking happens
> at runtime, yes?

For DBC as implemented in Eiffel, yes.

> Wouldn't it be possible to do them at compile time? (Although
> this raises decidability issues.)

It is certainly possible to prove statically that some assertions cannot fail.

The ESC/Java 2 (http://secure.ucd.ie/products/opensource/ESCJava2/docs.html)
tool for JML (http://www.cs.iastate.edu/~leavens/JML/) is one system that does
this -- although some limitations and usability problems are described in
<http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/papers/CASSIS2004.pdf>.

> Mightn't it also be possible to
> leave it up to the programmer whether a given contract
> was compile-time or runtime?

That would be possible, but IMHO a better option would be for an IDE to give
an indication (by highlighting, for example), which contracts are dynamically
checked and which are static.

This property is, after all, not something that the program should depend on.
It is determined by how good the static checker currently is, and we want to be
able to improve checkers (and perhaps even allow them to regress slightly in
order to simplify them) without changing programs.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>