On Fri, 04 Dec 2009 16:13:53 +0300, Michal Minich <michal.min...@gmail.com> wrote:

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?


Yes (it's already allowed in DMD trunk).

If exception handling postcondition is empty (or does not throw any Error or Exception), should the exception throw in body be suppressed or not? If you throw in postcondition, what to do with Exception throw in body ?


I guess that's what exception chaining is for.

Reply via email to