should postconditions be evaluated even if Exception is thrown?

[Pelle Månsson]

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.
> 
> 
> Andrei
Isn't the post-condition mainly to assert the correctness of the return 
value? Or at least partially? The output cannot be correct if an 
exception is thrown, so any assertion in the post condition concerning 
the output would fail by definition, right?

I would say the invariant() is the correct part to run.