Enforcing assertions in Eiffel

[Joachim Durchholz <joachim.durchholz@munich.netsurf.de>]

Joerg Rodemann wrote:
> 
> Well, sorry to raise this topic again, we had a long discussion about
> that
> shortly and it's still continuing, but this seems to point to some
> problems
> we discussed in a concrete situation: 

Well, no - I can't imagine what the GPL (a *legal* contract) has to do
with Eiffel assertions (a *technical* contract).

> how is the Eiffel system going
> to check
> the usage of a class versus its specification (seems we agreed on the
> term
> short-flat form as a similar concept to the Ada spec.) Is the Eiffel
> system
> able to check against the compiled library or is it more likely to
> leave that
> to the linker as in C++?

Eiffel assertions are predicates, which in the language context means
boolean expressions. If the proper options are set at compile time these
expressions will be evaluated at the appropriate time; a violated
assertion will raise an exception.
Needless to say that these exceptions shouldn't be called to "fix things
up" in any way - what should be fixed is the code, not the execution. Of
course such an exception might still be caught to prevent disaster, e.g.
in an embedded system to safely shut down the machine or to fall back to
some panic mode of operation, or in an interactive system to report the
error and ask the user to try something different.

One important side note: You can compile each class with its individual
level of assertion checking (preconditions, postconditions, invariants,
and a few other assertion types not relevant on the interface level).
However, precondition checks are done in the caller (at least
conceptually), so even if you use a library compiled with all checks
off, you can still run your code with precondition checking on and
you'll get exceptions if you call that library with (say) wrong
parameters.

Regards,
Joachim
-- 
Please don't send unsolicited ads.