Re: should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Michal Minich wrote:
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?

Good point. Probably a pure function has no place to define an 
out(Exception) guarantee.

Similarly, when function is nothrow or when is not marked pure but does 
not make any side effect either.

Such functions may choose to simply omit the out(Exception) clause.


Andrei