should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Michiel Helvensteijn wrote:
> 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.
> 

Yah, I was thinking of something along the same lines.

Andrei