What is a type error?

[Marshall]

Joachim Durchholz wrote:
> Marshall schrieb:
>
> > I can certainly see how DbC would be useful without subtyping.
> > But would there still be a reason to separate preconditions
> > from postconditions? I've never been clear on the point
> > of differentiating them (beyond the fact that one's covariant
> > and the other is contravariant.)
>
> There is indeed.
> The rules about covariance and contravariance are just consequences of
> the notion of having a subtype (albeit important ones when it comes to
> designing concrete interfaces).
>
> For example, if a precondition fails, something is wrong about the
> things that the subroutine assumes about its environment, so it
> shouldn't have been called. This means the error is in the caller, not
> in the subroutine that carries the precondition.
>
> The less important consequence is that this should be reflected in the
> error messages.
>
> The more important consequences apply when integrating software.
> If you have a well-tested library, it makes sense to switch off
> postcondition checking for the library routines, but not their
> precondition checking.
> This applies not just for run-time checking: Ideally, with compile-time
> inference, all postconditions can be inferred from the function's
> preconditions and their code. The results of that inference can easily
> be stored in the precompiled libraries.
> Preconditions, on the other hand, can only be verified by checking all
> places where the functions are called.

Interesting!

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?

And what's an invariant anyway?


Marshall