Walter Bright <[email protected]> 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. >
I would think that if a method in a class throws then at least the class' invariant should be run? does it?
