should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Walter Bright wrote:
> Andrei Alexandrescu wrote:
>> An exception (not an Error) is an expected and documented outcome of a 
>> function. After having listened to those endless Boeing stories, 
>> please listen to this one :o). Contract Programming covers the 
>> correctness of a program, and exceptions are correct behavior. By your 
>> very Boeing stories that I stoically endured, it seems like the 
>> logical conclusion is that postconditions must be evaluated upon 
>> exceptional return.
> 
> Consider a constructor. It's postcondition is the class invariant is 
> satisfied. If it throws, the object is not successfully constructed and 
> the invariant does not hold.

I agree. But constructors and destructors are already special, so that 
doesn't count. A regular function's postcondition should specify how it 
leaves the world in case an exception is passing through it.

string readAllText(File input)
out {
     assert(!input.isOpen());
}
body {
     ....
}



Andrei