should postconditions be evaluated even if Exception is thrown?

[Don]

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.

I think it has to. Otherwise, how can the caller restore the invariant?
Note that once the invariant is invalid, it can't call any member 
functions! The only thing it could do is delete the object.