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?
Similarly, when function is nothrow or when is not marked pure but does not make any side effect either.
