On 2009-12-04 04:11:22 -0500, Michal Minich <[email protected]> said:
Hello Andrei,
The way I was thinking of it is:
int f()
out(result) { }
out(Exception e) { }
body { }
So you have a chance to assert what the world looks like in case you
plan on returning a result, and what the world looks like if an
exception is emerging from the function.
So checked exceptions - this is not.
Andrei
if the function which throws exception is pure, then there is no world
invariant to hold on after function exits (only return value is to be
checked on success). Is there reason to have out(Exception ex) {}
postcondition for pure function, or it should be compile time error to
specify one?
Well you could still assert something about the exception:
out (LoginException ex) { assert(ex.errorDescription != ""); }
So, although I can't really find an example that looks useful, someone
might and I don't think it should be disallowed.
Similarly, when function is nothrow or when is not marked pure but does
not make any side effect either.
In a nothrow function it certainly does not make sense have contracts
for exceptions since none can be thrown. The only reasonable thing you
could do in one is this:
out (Exception e) { assert(false); }
But since the compiler can statically check that no exception can be
thrown it's dead code anyway... unless someone cast a function that
throws as nothrow.
--
Michel Fortin
[email protected]
http://michelf.com/
