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
