should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

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