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.
I agree with Andrei on this one. If there's some part of the object that's allowed to be in a 'bad' state, then it shouldn't be part of the invariant nor checked in the out contract. But it _should_ be possible for someone to construct an object that is strongly consistent including in the face of exceptions and have the DbC aspects of D help enforce that. Later, Brad
