Re: Ensuring postconditions in the face of exceptions

[AdaMagica <christoph.grein@eurocopter.com>]

> generic
>    with procedure Visit (Object : in out T);
> procedure Refresh (Object : in out T; Dirty : access Boolean) is
> begin
>    if Dirty then
>       Visit (Object);
>       Dirty := False;
>    end if;
> exception
>    when others =>
>       Dirty := True; -- warnings here
>       raise;
> end Refresh;

This is the proposed solution, I guess. I've got problems with this.
As fas as I understand the RM, the compiler is free to replace a
complete block of code by just raising the exception if it can prove
that the exception will be raised.

So how then can you be sure that the parameter Dirty is set as you
expect? An exception is an exceptional case (say what!), so I do not
see how you can define normal postconditions for any parameters
(scalars don't work as the compiler has told you - and for others, see
above).