Andrei Alexandrescu wrote:
Pelle Månsson 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
Isn't the post-condition mainly to assert the correctness of the
return value? Or at least partially? The output cannot be correct if
an exception is thrown, so any assertion in the post condition
concerning the output would fail by definition, right?
I would say the invariant() is the correct part to run.
As others have mentioned, you may have different postconditions
depending on whether an exception was thrown or not.
I think a major failure of exceptions as a language mechanism is that
they gave the illusion that functions need not worry about what happens
when an exception traverses them, and only need to focus on the success
case.
Andrei
In the case of special postconditions for exceptions, I agree it should
be there. Something to replace the finally.
