On Thu, 03 Dec 2009 13:47:25 -0500, Andrei Alexandrescu
<seewebsiteforem...@erdani.org> wrote:
Don wrote:
Andrei Alexandrescu wrote:
Michiel Helvensteijn wrote:
Andrei Alexandrescu wrote:
This may sound crazy, but if you just follow the facts that
distinguish
regular error handling from program correctness, you must live with
the
consequences. And the consequence is - a function's postcondition
must
be designed to take into account exceptional paths. Only in case of
unrecoverable errors is the function relieved of its duty.
You don't want the regular postcondition to express exceptional
outcomes.
However, there *should* be an exception-postcondition clause, which
describes the conditions which are guaranteed to hold after an
exception is
thrown.
int f() throws (SomeException, SomeOtherException)
pre { }
body { }
post(int result) { }
epost(SomeException x) { }
epost(SomeOtherException)x) { }
I believe JML does something like this.
Yah, I was thinking of something along the same lines.
Andrei
Yup. It's checked exceptions.
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.
That looks fine to me as long as
out(Exception e)
is optional -- it should revert to the original behavior.
-Steve
