should postconditions be evaluated even if Exception is thrown?

[Michal Minich]

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.