Re: Ensuring postconditions in the face of exceptions

[Robert Matthews <ignored@ramatthews.free-online.co.uk>]

Jeffrey R. Carter wrote:

> Ludovic Brenta wrote:
>> 
>> The problem with that approach is that the processing of the Dirty
>> flag is no longer localized in the Refresh procedure which, in fact,
>> might as well disappear altogether; instead, each caller of Refresh
>> (or Visit) must now remember to handle exceptions and reset Dirty to
>> True accordingly.
> 
> With your code, the only way an exception can be raised is if the input
> value of Dirty is True. Since Dirty is not a parameter of Visit, the call
> to Visit presumably doesn't change Dirty. If so, you could eliminate the
> exception handler and have the desired functionality: Dirty would be True
> on return if there were an exception, and False if there were not. I think
> this was mentioned before. Is there a reason this is not acceptable?
> 

By which I presume the code could be:

generic
   with procedure Visit (Object : in out T);
procedure Refresh (Object : in out T; Dirty : in out Boolean) is
begin
   if Dirty then
      Visit (Object);
      Dirty := False;
   end if;
end Refresh;

Looks to be the simplest approach to me, though Bob Duff's
suggestion of a Cache type may be a better abstraction.

Robert Matthews