should postconditions be evaluated even if Exception is thrown?

[Michal Minich]

Hello Michel,

>> 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?
>> 
> Well you could still assert something about the exception:
> 
> out (LoginException ex) { assert(ex.errorDescription != ""); }
> 
> So, although I can't really find an example that looks useful, someone
> might and I don't think it should be disallowed.

Yes, you could provide more specific error message (or maybe throw more specific 
exception), but I'm not sure how useful is this.

I'm also not sure about how some specifics should work:

currently, it is not allowed to throw Exception from postcondition, it is 
only possible to throw Error (assert). Should it be possible to throw Exception 
from error handling postcondition or not?

If exception handling postcondition is empty (or does not throw any Error 
or Exception), should the exception throw in body be suppressed or not? 

If you throw in postcondition, what to do with Exception throw in body ?
 
>> Similarly, when function is nothrow or when is not marked pure but
>> does not make any side effect either.
>> 
> In a nothrow function it certainly does not make sense have contracts
> for exceptions since none can be thrown. The only reasonable thing you
> could do in one is this:
> 
> out (Exception e) { assert(false); }
> 
> But since the compiler can statically check that no exception can be
> thrown it's dead code anyway... unless someone cast a function that
> throws as nothrow.
> 

but function and it contracts are defined at compile time anyway. (Such nothrow 
cast could only badly affect callers of this function.)