On Thu, 03 Dec 2009 06:51:32 +0300, Andrei Alexandrescu
<seewebsiteforem...@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.
