should postconditions be evaluated even if Exception is thrown?

[Denis Koroskin]

On Fri, 04 Dec 2009 16:35:57 +0300, Leandro Lucarella <llucax at gmail.com>  
wrote:

> Michal Minich, el  4 de diciembre a las 13:13 me escribiste:
>> 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?
>
> I don't think so, postconditions should not change the programs behavior,
> it's like asserts or any other DbC feature. You can compile the program
> without it, and it should work the same.
>
> I think postconditions should only be able to inspect (in a read-only
> manner) the exception; once the postcondition finished executing, the
> exception should be propagated as is.
>
>> If exception handling postcondition is empty (or does not throw any
>> Error or Exception), should the exception throw in body be
>> suppressed or not?
>
> No.
>
>> If you throw in postcondition, what to do with Exception throw in body ?
>
> You can't throw in postconditions.
>

You can't throw in pre/postconditions, but it's a bug:

http://d.puremagic.com/issues/show_bug.cgi?id=3388
http://d.puremagic.com/issues/show_bug.cgi?id=3400