should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Denis Koroskin wrote:
> On Thu, 03 Dec 2009 06:51:32 +0300, Andrei Alexandrescu 
> <SeeWebsiteForEmail at erdani.org> 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
> 
> I'm not sure about post-conditions, but invariants have to be called. 
> Exception-safe programming is a must. Any function may fail, and in that 
> happens, the function should leave an object it operates on in a correct 
> state.
> 
> With post-conditions, there is a pitfall: if function throws an 
> exception, there is no return value, and nothing to verify. For example:
> 
> float sqrt(float value)
> out (result)
> {
>     assert(value * value == result);
> }
> body
> {
>     assert(value >= 0); // might throw. What value the 'result' variable 
> in a post-condition would store?
> 
>     return core.stdc.sqrt(value);
> }
> 
> Reading your post for a second time, I think you are confusing 
> post-condition with something else. How would you close a file in a 
> post-condition (or an invariant)? I believe both should be 
> @relaxedPure/hasNoSideEffects. File closing should be done in a function 
> body using scope (exit) mechanism.

The language would need to allow you to write an out(result) 
postcondition and an out(Exception) postcondition.

Andrei