should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Steven Schveighoffer wrote:
> On Thu, 03 Dec 2009 13:47:25 -0500, Andrei Alexandrescu 
> <SeeWebsiteForEmail at erdani.org> wrote:
> 
>> 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.
> 
> That looks fine to me as long as
> 
> out(Exception e)
> 
> is optional -- it should revert to the original behavior.
> 
> -Steve

I agree. To entirely accommodate existing behavior, out without an 
argument should only be evaluated if an exception is not thrown.

Andrei