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:
> > 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.
>
> OK, then Dirty is a property of the cache.  So how about:
>
>     type Cache is limited
>         record
>             X : T;
>             Dirty : Boolean := True;
>         end record;
>     type Cache_Ref is access all Cache;
>
> and pass a parameter of type Cache_Ref?  (Or perhaps
> X could be an access type, and point to the T object.)
>
> You need to pass some sort of pointer, explicitly or implicitly,
> because when you raise an exception, the copy-back is skipped.
> You said that relying on limitedness to force pass-by-referrence
> is confusing -- I agree.  So pass an explicit pointer.
>
> I recommend a named access type, because anonymous access parameters
> have dynamic accessibility, which is a tripping hazard, and is
> less efficient.

Yes, that's the solution I have, currently, i.e. (5); except that the
Cache type already existed before, has other unrelated components and
is not limited.

--
Ludovic Brenta.