Walter Bright 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.
I have a hard time accepting this as a requirement. An exception means
it failed, not succeeded.
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.
Andrei
