should postconditions be evaluated even if Exception is thrown?

[Brad Roberts]

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