should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Don wrote:
> 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.

The way I was thinking of it is:

int f()
out(result) { }
out(Exception e) { }
body { }

So you have a chance to assert what the world looks like in case you 
plan on returning a result, and what the world looks like if an 
exception is emerging from the function.

So checked exceptions - this is not.


Andrei