Re: Ada vs Eiffel - Ada programmer approach

["Hibou57 (Yannick Duchêne)" <yannick_duchene@yahoo.fr>]

On 26 mai, 15:37, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote:
> [...] Ada's pragma Assert provides what I
> need in these (rare) cases  because I can put such pragmas in the
> middle of a subprogram, for example.
>
> --
> Ludovic Brenta.

This is not the same as Eiffel assertions. Eiffel's assertions are
aware of the invokation contexte. Let say you have a class C and a
method M and the class C has an invariant I. Then, if a client invoks
M, the invariant will be checked before M returns. That's Ok, this is
the same as with "in code assertions". But if M is invoked by anoher
method of the class, i.e. as an implementation method (this is very
common to use a public method for internal purpose), you will have
this : the client of C invok a method M2 which in turn will invok M
(the client may or may not know about it). In this context, the class
invariant will obviously be checked before returning from M2, but *it
will not be check before return from M*.

That is beceause M is allowed to left the class invariant in an
illegal state, as it may be the sole responsability of M2.

So, Eiffel's assertions are not the same as "in code assertions".
Eiffel's assertions are well formalized.