Exception postcondition?

[Michiel Helvensteijn]

Hi,

In Eiffel, a postcondition describes what a routine guarantees if it
terminates normally. Is there a similar clause which can describe the
guarantees when an exception is thrown?

--
Michiel Helvensteijn

[none]

Michiel Helvensteijn a �crit :

> Hi,
>
> In Eiffel, a postcondition describes what a routine guarantees if it
> terminates normally. Is there a similar clause which can describe the
> guarantees when an exception is thrown?
>

Exception code is supposed to run a trick that allows function to ensure
its postcondition. Having a postcondition per exception would be a huge
mess! I suppose this is why it is not permitted.

Guillaume

[Helmut]

On Aug 26, 5:47 am, Michiel Helvensteijn

No and yes. In a normal situation a routine is obliged to fulfill its
postcondition. If it cannot for whatever reason, it must not terminate
normally, it has to throw an exception.

If a routine throws an exception, its rescue clause is entered. The
obligation of the rescue clause is to establish the class invariant
(this you can regard as a kind of guarantee, the routine has to give).

A rescue clause either ends in a retry (the routine gets a second
chance to fulfill its contract) or not. Not ending in retry causes the
routine to fail and the exception processing continues in the calling
routine and soon. If there is no retry up to the the root procedure,
the whole program fails because of an unhandled exception. I.e. the
only way to handle an exception succcessfully is to enter a retry!