Re: Ensuring postconditions in the face of exceptions

[Alex Mentis <asmentis@gmail.com>]

On Mar 12, 4:13 am, Ludovic Brenta <ludo...@ludovic-brenta.org> 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;
>
> GNAT says:
> warning: assignment to pass-by-copy formal may have no effect
> warning: "raise" statement may result in abnormal return (RM
> 6.4.1(17))
>
> The reason for the exception handler is to enforce a postcondition
> that Dirty must be True if Visit raises an exception. However the
> warnings suggest that the postcondition cannot be enforced this way.
> How should I rewrite my code?
>
> --
> Ludovic Brenta.

I think trying to "force" the parameter passing mode to a certain mode
is making this more complicated than necessary.  One of the nice
things about Ada over other languages is that you generally shouldn't
have to worry about whether a parameter is copy-by-value or copy-by-
reference.

In this case, you are trying to use the exception handler to assign a
value to the local parameter Dirty so that it can get passed back to
the calling subprogram.  This implies the calling subprogram has a
parameter in its scope that keeps track of dirtiness, too.  Instead of
trying to set Dirty to True in Refresh, why not just raise a user-
defined exception (such as Dirty_Error) and have an exception handler
in the calling subprogram that catches this exception and sets the
*calling subprogram's* variable tracking dirtiness to True?

Alex