should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Don 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.
>>
>>
>> Andrei
> 
> If you mean that all class invariants must be satisfied regardless of 
> exceptions, then I agree.
> But if you mean the function postcondition, I don't think that makes 
> sense. If the file needs to be closed, that should be part of the File 
> invariant.

The file invariant can't be "the file is closed". A free function 
readAllText(File f) could say that the postcondition is that the file is 
closed, even though a UTF exception does get thrown.

Andrei