should postconditions be evaluated even if Exception is thrown?

[Denis Koroskin]

On Fri, 04 Dec 2009 16:13:53 +0300, Michal Minich  
<michal.minich at gmail.com> wrote:

> 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?
>

Yes (it's already allowed in DMD trunk).

> 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 ?
>

I guess that's what exception chaining is for.