should postconditions be evaluated even if Exception is thrown?

[Michiel Helvensteijn]

Andrei Alexandrescu wrote:

> This may sound crazy, but if you just follow the facts that distinguish
> regular error handling from program correctness, you must live with the
> consequences. And the consequence is - a function's postcondition must
> be designed to take into account exceptional paths. Only in case of
> unrecoverable errors is the function relieved of its duty.

You don't want the regular postcondition to express exceptional outcomes.

However, there *should* be an exception-postcondition clause, which
describes the conditions which are guaranteed to hold after an exception is
thrown.

int f() throws (SomeException, SomeOtherException)
pre { }
body { }
post(int result) { }
epost(SomeException x) { }
epost(SomeOtherException)x) { }

I believe JML does something like this.

-- 
Michiel Helvensteijn