should postconditions be evaluated even if Exception is thrown?

[Don]

Andrei Alexandrescu wrote:
> 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

Yup. It's checked exceptions.