What is a type error?

[Joachim Durchholz]

Marshall schrieb:
> So, what exactly separates a precondition from a postcondition
> from an invariant? I have always imagined that one writes
> assertions on parameters and return values, and those
> assertions that only reference parameters were preconditions
> and those which also referenced return values were postconditions.
> Wouldn't that be easy enough to determine automatically?

Sure.
Actually this can be done in an even simpler fashion; e.g. in Eiffel, it 
is (forgive me if I got the details wrong, it's been several years since 
I last coded in it):

   foo (params): result_type is
   require
     -- list of assertions; these become preconditions
   do
     -- subroutine body
   ensure
     -- list of assertions; these become postconditions
   end

> And what's an invariant anyway?

In general, it's a postcondition to all routines that create or modify a 
data structure of a given type.

Eiffel does an additional check at routine entry, but that's just a 
last-ditch line of defense against invariant destruction via aliases, 
not a conceptual thing. Keep aliases under control via modes (i.e. 
"unaliasable" marks on local data to prevent aliases from leaving the 
scope of the data structure), or via locking, or simply by disallowing 
destructive updates, and you don't need the checks at routine entry anymore.

Regards,
Jo