Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta <ludovic@ludovic-brenta.org>]

Robert A Duff wrote on comp.lang.ada:
> Ludovic Brenta <ludo...@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)?

Yes, that is correct.

> 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)?

No, Dirty is not a property of the object; the type T is used in
several places, only some of which (a one-line cache, essentially) has
a Dirty property.

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

I agree; this generalizes my question even more.

--
Ludovic Brenta.