On Fri, 04 Dec 2009 16:35:57 +0300, Leandro Lucarella <llu...@gmail.com>
wrote:
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.
You can't throw in pre/postconditions, but it's a bug:
http://d.puremagic.com/issues/show_bug.cgi?id=3388
http://d.puremagic.com/issues/show_bug.cgi?id=3400
