should postconditions be evaluated even if Exception is thrown?

[Leandro Lucarella]

Michal Minich, el  4 de diciembre a las 13:13 me escribiste:
> Hello Michel,
> 
> >>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.
> 
> Yes, you could provide more specific error message (or maybe throw
> more specific exception), but I'm not sure how useful is this.
> 
> I'm also not sure about how some specifics should work:
> 
> currently, it is not allowed to throw Exception from postcondition,
> it is only possible to throw Error (assert). Should it be possible
> to throw Exception from error handling postcondition or not?

I don't think so, postconditions should not change the programs behavior,
it's like asserts or any other DbC feature. You can compile the program
without it, and it should work the same.

I think postconditions should only be able to inspect (in a read-only
manner) the exception; once the postcondition finished executing, the
exception should be propagated as is.

> If exception handling postcondition is empty (or does not throw any
> Error or Exception), should the exception throw in body be
> suppressed or not?

No.

> If you throw in postcondition, what to do with Exception throw in body ?

You can't throw in postconditions.

-- 
Leandro Lucarella (AKA luca)                     http://llucax.com.ar/
----------------------------------------------------------------------
GPG Key: 5F5A8D05 (F8CD F9A7 BF00 5431 4145  104C 949E BFB6 5F5A 8D05)
----------------------------------------------------------------------
G: I don't want hope. Hope is killing me. My dream is to become
   hopeless. When you're hopeless you don't care. And when you
   care, that indifference makes you attractive.
J: So, hopelessness is the key?
G: It's my only hope.
	-- George Constanza & Jerry Seinfeld