should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Walter Bright wrote:
> Brad Roberts wrote:
>> Walter Bright wrote:
>>> Rory McGuire wrote:
>>>> I would think that if a method in a class throws then at least the
>>>> class' invariant should be run? does it?
>>> No.
>>
>> Do you consider that broken or correct?
> 
> 
> Not sure.

TDPL says that in non-release mode, public methods have code 
instrumented like this:

class C {
    void m() {
       __check_invariant();
       scope(exit) __check_invariant();
       ... body ...
    }
}

My understanding after a recent discussion to Walter focused on the 
topic is that in case a non-Exception Error is thrown, scope(exit) 
statements are not guaranteed to be executed, as aren't destructors of 
local objects and finally clauses.


Andrei