should postconditions be evaluated even if Exception is thrown?

[Sean Kelly]

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.

Postconditions serve two purposes in my mind: to verify that object details are in a valid state when this checking isn't possible or appropriate in an invariant, and to check that the return value is in range.  It seems quite reasonable to want the object validation to occur, but impossible for return value checking to occur... unless a feature is added to test if an exception is in flight and then expect the user to call this in postconditions to see if they should omit return value checking.  This seems like it may be too onerous of a requirement.