Re: Ensuring postconditions in the face of exceptions

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

Ludovic Brenta <ludovic@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.

- Bob