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
