should postconditions be evaluated even if Exception is thrown?
Don
nospam at nospam.com
Thu Dec 3 00:28:40 PST 2009
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.
More information about the Digitalmars-d
mailing list