should postconditions be evaluated even if Exception is thrown?

[Rory McGuire]

Walter Bright <newshound1 at digitalmars.com> wrote:
 
> Andrei Alexandrescu wrote:
>> If a function throws a class inheriting Error but not Exception (i.e. an 
>> unrecoverable error), then the postcondition doesn't need to be satisfied.
>> 
>> I just realized that postconditions, however, must be satisfied if the 
>> function throws an Exception-derived object. There is no more return 
>> value, but the function must leave everything in a consistent state. For 
>> example, a function reading text from a file may have the postcondition 
>> that it closes the file, even though it may throw a malformed file 
>> exception.
>> 
>> This may sound crazy, but if you just follow the facts that distinguish 
>> regular error handling from program correctness, you must live with the 
>> consequences. And the consequence is - a function's postcondition must 
>> be designed to take into account exceptional paths. Only in case of 
>> unrecoverable errors is the function relieved of its duty.
> 
> I have a hard time accepting this as a requirement. An exception means 
> it failed, not succeeded.
> 

I would think that if a method in a class throws then at least the class' 
invariant should be run? does it?