should postconditions be evaluated even if Exception is thrown?

[Pelle Månsson]

Andrei Alexandrescu wrote:
> Pelle Månsson 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
>> Isn't the post-condition mainly to assert the correctness of the 
>> return value? Or at least partially? The output cannot be correct if 
>> an exception is thrown, so any assertion in the post condition 
>> concerning the output would fail by definition, right?
>>
>> I would say the invariant() is the correct part to run.
> 
> As others have mentioned, you may have different postconditions 
> depending on whether an exception was thrown or not.
> 
> I think a major failure of exceptions as a language mechanism is that 
> they gave the illusion that functions need not worry about what happens 
> when an exception traverses them, and only need to focus on the success 
> case.
> 
> 
> Andrei
In the case of special postconditions for exceptions, I agree it should 
be there. Something to replace the finally.