should postconditions be evaluated even if Exception is thrown?

[Michel Fortin]

On 2009-12-04 04:11:22 -0500, Michal Minich <michal.minich at gmail.com> 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
michel.fortin at michelf.com
http://michelf.com/