should postconditions be evaluated even if Exception is thrown?

[Walter Bright]

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.