should postconditions be evaluated even if Exception is thrown?

[Denis Koroskin]

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.