should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Michal Minich wrote:
> Hello Andrei,
> 
>> 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
>>
> 
> if the function which throws exception is pure, then there is no world 
> invariant to hold on after function exits (only return value is to be 
> checked on success). Is there reason to have out(Exception ex) {} 
> postcondition for pure function, or it should be compile time error to 
> specify one?

Good point. Probably a pure function has no place to define an 
out(Exception) guarantee.

> Similarly, when function is nothrow or when is not marked pure but does 
> not make any side effect either.

Such functions may choose to simply omit the out(Exception) clause.


Andrei