Denis Koroskin wrote:
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.
The language would need to allow you to write an out(result)
postcondition and an out(Exception) postcondition.
Andrei