Re: Ensuring postconditions in the face of exceptions

[Georg Bauhaus <see.reply.to@maps.futureapps.de>]

Dmitry A. Kazakov wrote:
> On Fri, 12 Mar 2010 01:13:45 -0800 (PST), Ludovic Brenta wrote:
> 
>> Consider the procedure:
>>
>> type T is private; -- completion elided
>>
>> generic
>>    with procedure Visit (Object : in out T);
>> procedure Refresh (Object : in out T; Dirty : in out T) is
>> begin
>>    if Dirty then
>>       Visit (Object);
>>       Dirty := False;
>>    end if;
>> exception
>>    when others =>
>>       Dirty := True; -- warnings here
>>       raise;
>> end Refresh;
> 
> Poor design IMO. Either Dirty is a property of the object, then it must be 
> a member of T. Otherwise it is a result of Refresh for the caller, who 
> don't need Dirty flag anyway, because when exception propagates, he knows 
> that something was wrong.

Agree.  Reminds me of a "rescue clause" as in Eiffel DbC that
you use IFF trying to remove the cause of the previous exception
and then trying the subp/block again. If there is no need to retry and
you just record some state in Dirty, then why raise?  OTOH, if the
caller needs to be informed about the nature of the exception,
that information could be part of a suitably defined state parameter.