Re: Ensuring postconditions in the face of exceptions

[Robert A Duff <bobduff@shell01.TheWorld.com>]

Ludovic Brenta <ludovic@ludovic-brenta.org> writes:

> That's an interesting suggestion but we've patched the run-time library
> so that it dumps core on every exception;...

Then how can it ever get to the "when others" in Refresh?
Or do you mean it dumps core, and then the program continues
on past the point of the bug (propagates the exception,
handles it, etc)?

Is "dirty" a property of the object being visited?
If so, would it make sense to make it a component
of that object, and make sure that is passed by
reference (either by explicitly passing a pointer,
or by making the type limited or tagged)?

By the way, I think it makes perfect sense to have
different postconditions for normal return, and for
each exception that might be raised.

- Bob