Ensuring postconditions in the face of exceptions

Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

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.

Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

Ludovic Brenta wrote on comp.lang.ada:
> 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

Sorry, I meant:

procedure Refresh (Object : in out T; Dirty : in out Boolean) 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.

Re: Ensuring postconditions in the face of exceptions

[Niklas Holsti]

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;
> 
> 
> 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?

Perhaps change the mode of Dirty to

    Dirty : access T;

and assign

    Dirty.all := True;

Or use a named access type instead of the anonymous access, as you prefer.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

On Mar 12, 10:29 am, Niklas Holsti <niklas.hol...@tidorum.invalid>
wrote:
> 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;
>
> > 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?
>
> Perhaps change the mode of Dirty to
>
>     Dirty : access T;
>
> and assign
>
>     Dirty.all := True;
>
> Or use a named access type instead of the anonymous access, as you prefer.

Heh. I was kind of hoping you wouldn't say that :) I should have been
more specific; I think using an access type is ugly but I can't think
of a better solution.

Thanks.

--
Ludovic Brenta.

Re: Ensuring postconditions in the face of exceptions

[Jeffrey R. Carter]

Ludovic Brenta wrote:
> 
> Heh. I was kind of hoping you wouldn't say that :) I should have been
> more specific; I think using an access type is ugly but I can't think
> of a better solution.

Use a limited type:

type Dirty_Info is limited record
    Value : Boolean := False;
end record;

procedure Refresh (Object : in out T; Dirty : in out Dirty_Info);
...
    if Dirty.Value then
...
    Dirty.Value := True;

Parameters of limited types are passed by reference.

-- 
Jeff Carter
"What I wouldn't give for a large sock with horse manure in it."
Annie Hall
42

Re: Ensuring postconditions in the face of exceptions

[Randy Brukardt]

"Jeffrey R. Carter" <spam.jrcarter.not@spam.acm.org> wrote in message 
news:hndhls$3ns$1@tornado.tornevall.net...
> Ludovic Brenta wrote:
>>
>> Heh. I was kind of hoping you wouldn't say that :) I should have been
>> more specific; I think using an access type is ugly but I can't think
>> of a better solution.
>
> Use a limited type:
>
> type Dirty_Info is limited record
>    Value : Boolean := False;
> end record;
>
> procedure Refresh (Object : in out T; Dirty : in out Dirty_Info);
> ...
>    if Dirty.Value then
> ...
>    Dirty.Value := True;
>
> Parameters of limited types are passed by reference.

For the record, I think you mean "limited record types". There are no 
requirements on how limited private types or record types that happen to be 
limited because of a limited component are passed.


                          Randy.

Re: Ensuring postconditions in the face of exceptions

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> For the record, I think you mean "limited record types". There are no 
> requirements on how limited private types or record types that happen to be 
> limited because of a limited component are passed.

Well, that needs some clarification:  for example, a record containing
a task is passed by reference, even if the record doesn't explicitly
say "limited".

The point is, the compiler looks at the full types of everything
involved when deciding whether it must pass something by reference.
So "limited private" is irrelevant.

- Bob

Re: Ensuring postconditions in the face of exceptions

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wcc7hpgckyy.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> For the record, I think you mean "limited record types". There are no
>> requirements on how limited private types or record types that happen to 
>> be
>> limited because of a limited component are passed.
>
> Well, that needs some clarification:  for example, a record containing
> a task is passed by reference, even if the record doesn't explicitly
> say "limited".
>
> The point is, the compiler looks at the full types of everything
> involved when deciding whether it must pass something by reference.
> So "limited private" is irrelevant.

I missed a word: I meant "explicitly limited record type" (that is one that 
contains the word "limited" in the record declaration). That and "tagged" 
are the only ways to *guarantee* that a record is passed by reference.

Jeff Carter writes:
>Really? ARM 6.2 seems to me to say that any limited type (a type whose full 
>view
>is limited) is passed by reference. This explicitly includes a composite 
>type
>with a component of a limited type.

You suddenly added "full view" to this, and that's the crux of the problem: 
"limited" is a property of a view, while "by-reference" is a property of a 
type. (BTW, 6.2(7) is subtly broken, see AI05-0096-1 for details if you're 
Adam or want to know every possible detail. :-) The point is that there are 
many limited types that are not required to be passed by reference, 
including some record types that are limited.

Also note that your statement here is also subtly wrong: a record type has 
to be passed by reference if it has a by-reference component -- not a 
limited component! A component of a limited private type would make the 
record limited but not necessarily by-reference (read the rules carefully 
again).

Repeat after me: "limited" is a property of a view! It's not constant for a 
particular type! That's a common mistake that even those of us on the ARG 
make from time-to-time.

                                      Randy.

Re: Ensuring postconditions in the face of exceptions

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> "Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
> news:wcc7hpgckyy.fsf@shell01.TheWorld.com...
>> "Randy Brukardt" <randy@rrsoftware.com> writes:
>>
>>> For the record, I think you mean "limited record types". There are no
>>> requirements on how limited private types or record types that happen to 
>>> be
>>> limited because of a limited component are passed.
>>
>> Well, that needs some clarification:  for example, a record containing
>> a task is passed by reference, even if the record doesn't explicitly
>> say "limited".
>>
>> The point is, the compiler looks at the full types of everything
>> involved when deciding whether it must pass something by reference.
>> So "limited private" is irrelevant.
>
> I missed a word: I meant "explicitly limited record type" (that is one that 
> contains the word "limited" in the record declaration). That and "tagged" 
> are the only ways to *guarantee* that a record is passed by reference.

That's still not quite right.  A record that contains a task, protected,
or a tagged component is passed by ref, even if the record
is not explicitly limited.

See RM-6.2.

> Jeff Carter writes:
>>Really? ARM 6.2 seems to me to say that any limited type (a type whose full 
>>view
>>is limited) is passed by reference. This explicitly includes a composite 
>>type
>>with a component of a limited type.

...with a component of a by-ref type.

> You suddenly added "full view" to this, and that's the crux of the problem: 
> "limited" is a property of a view, while "by-reference" is a property of a 
> type. (BTW, 6.2(7) is subtly broken, see AI05-0096-1 for details if you're 
> Adam or want to know every possible detail. :-) The point is that there are 
> many limited types that are not required to be passed by reference, 
> including some record types that are limited.

Right.  Example: record containing a component of a limited private
type, whose full type is scalar.

> Also note that your statement here is also subtly wrong: a record type has 
> to be passed by reference if it has a by-reference component -- not a 
> limited component! A component of a limited private type would make the 
> record limited but not necessarily by-reference (read the rules carefully 
> again).
>
> Repeat after me: "limited" is a property of a view! It's not constant for a 
> particular type! That's a common mistake that even those of us on the ARG 
> make from time-to-time.

I don't understand why the definition of "by reference" is subtly
different from the definition of "immutably limited".

- Bob

Re: Ensuring postconditions in the face of exceptions

[Adam Beneschan]

On Mar 16, 8:18 am, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:

> > Repeat after me: "limited" is a property of a view! It's not constant for a
> > particular type! That's a common mistake that even those of us on the ARG
> > make from time-to-time.
>
> I don't understand why the definition of "by reference" is subtly
> different from the definition of "immutably limited".

Well, for one thing, the language defines what types are "immutably
limited", but it doesn't completely define which types are "by
reference"---the implementation decides that in some cases (6.2(11)).

                          -- Adam

Re: Ensuring postconditions in the face of exceptions

[Robert A Duff]

Adam Beneschan <adam@irvine.com> writes:

> On Mar 16, 8:18�am, Robert A Duff <bobd...@shell01.TheWorld.com>
> wrote:
>
>> > Repeat after me: "limited" is a property of a view! It's not constant for a
>> > particular type! That's a common mistake that even those of us on the ARG
>> > make from time-to-time.
>>
>> I don't understand why the definition of "by reference" is subtly
>> different from the definition of "immutably limited".
>
> Well, for one thing, the language defines what types are "immutably
> limited", but it doesn't completely define which types are "by
> reference"---the implementation decides that in some cases (6.2(11)).

I mean the term "by-reference type", which is (portably) defined by
the RM.  These are the types that are required to be passed by
reference.

You're right that there are some other types where the compiler
gets to decide -- but I wasn't talking about those.

- Bob

Re: Ensuring postconditions in the face of exceptions

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wcciq8wxpkv.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
...
>> Repeat after me: "limited" is a property of a view! It's not constant for 
>> a
>> particular type! That's a common mistake that even those of us on the ARG
>> make from time-to-time.
>
> I don't understand why the definition of "by reference" is subtly
> different from the definition of "immutably limited".

Two obvious reasons: "by-reference" predates "immutably limited" by more 
than 10 years, and besides there are non-limited types where are 
"by-reference" (non-limited tagged types). The latter also means that types 
with a component of a non-limited tagged type are "by-reference" as well. 
Finally (OK, I can't count), "by-reference" breaks privacy (thus only 
dynamic rules ought to depend on it; legality rules should never depend on 
the contents of the private part), while "immutably limited" doesn't break 
privacy and thus can be used in legality rules. "Immutably limited" is a 
direct property; it doesn't depend on type of components.

The net effect is that there isn't much similarity between the two concepts, 
nor their use.

                             Randy.

Re: Ensuring postconditions in the face of exceptions

[Jeffrey R. Carter]

Randy Brukardt wrote:
> 
> For the record, I think you mean "limited record types". There are no 
> requirements on how limited private types or record types that happen to be 
> limited because of a limited component are passed.

Really? ARM 6.2 seems to me to say that any limited type (a type whose full view 
is limited) is passed by reference. This explicitly includes a composite type 
with a component of a limited type.

-- 
Jeff Carter
"Why don't you bore a hole in yourself and let the sap run out?"
Horse Feathers
49

Re: Ensuring postconditions in the face of exceptions

[Stephen Leake]

Ludovic Brenta <ludovic@ludovic-brenta.org> writes:

> 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?

I don't see the point; Visit is not called if Dirty is not True, so
you don't need to do anything in an exception handler. So I would
rewrite it by deleting the exception handler, and maybe adding a
comment. 

Unless you meant the opposite; if Dirty is supposed to be changed to
False on exception from Visit, then you need to set Dirty in the
handler. But that doesn't seem to make sense, given what Dirty seems
to mean.

It would be clearer to localize the exception handler:

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

but that's minor.

-- 
-- Stephe

Re: Ensuring postconditions in the face of exceptions

[Georg Bauhaus]

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.

Re: Ensuring postconditions in the face of exceptions

[Alex Mentis]

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

Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

Alex Mentis writes:
> 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?

That's an interesting suggestion but we've patched the run-time library
so that it dumps core on every exception; we use exceptions only for
exceptional situations and dumping core freezes the system for 30
seconds to produce a file roughly 300 MiB in size.  So I would rather
not raise exceptions that are do not detect a bug.

-- 
Ludovic Brenta.

Re: Ensuring postconditions in the face of exceptions

[Alex Mentis]

On Mar 14, 10:21 am, Ludovic Brenta <ludo...@ludovic-brenta.org>
wrote:
> Alex Mentis writes:
> > 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?
>
> That's an interesting suggestion but we've patched the run-time library
> so that it dumps core on every exception; we use exceptions only for
> exceptional situations and dumping core freezes the system for 30
> seconds to produce a file roughly 300 MiB in size.  So I would rather
> not raise exceptions that are do not detect a bug.
>
> --
> Ludovic Brenta.

Well, I'm not sure I'm suggesting you raise extra exceptions, just
handle them in the calling subprogram instead of the called
subprogram.  You're already re-raising the exception with the called
subprogram exception handler:

> >> exception
> >>    when others =>
> >>       Dirty := True; -- warnings here
> >>       raise;

You don't have to create a user-defined exception.  Consider the
following code:

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;

-- This handler isn't necessary, but I put it here to help illustrate
-- the changes I'm recommending.
exception
   when others =>
      raise;
end Refresh;

*****

procedure Calls_Refresh is

   Obj : T;
   Calling_Scope_Dirty : Boolean;

begin

   -- potentially other code here

   Dirty_Handler_Block :
   begin

      Refresh(Obj, Calling_Scope_Dirty);

   exception
      when others =>
         Calling_Scope_Dirty : True;
         -- potentially other handler code here

   end Dirty_Handler_Block;

   -- potentially other code here

end Calls_Refresh;

Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

Alex Mentis wrote on comp.lang.ada:
> Well, I'm not sure I'm suggesting you raise extra exceptions, just
> handle them in the calling subprogram instead of the called
> subprogram.  You're already re-raising the exception with the called
> subprogram exception handler:

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.

So let me summarize the various suggestions so far:

(1) pass Dirty as "access" instead of "in out": works but, as you
nicely put it, "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."

(2) pass Dirty encapsulated in a limited record: also works but this
is even worse (IMHO) than "access" because it obscures the purpose of
the limited record type. I'd have to have 10 lines of comments just to
explain why there is a limited record type containing a single Boolean
component.

(3) make Dirty part of the object type T: the flag is necessary in
only one of the places where T is used; also T is serialized in
several places, so changing it is not a good idea.

(4) handle the exception in the caller: there is no longer a central
place for handling the  Dirty flag therefore future maintenance is
harder. As a side effect, the procedure Refresh loses most of its
purpose, so might as well disappear.

I came up with (5): place both Dirty and the Object to be visited in a
record type and pass an access value to that record. This is a
variation of (1); it is still ugly (IMHO) but the record type and the
access-to-record type already existed so the change to the code base
was minimal. Since, however, the existing record type contains many
other things besides the Object and Dirty flag, the procedure Refresh
receives much more information than it really needs, which might break
encapsulation.

All in all, no solution so far is as elegant as I would have liked but
thanks anyway for the various suggestions. I think that (1) is still
the least ugly though.

--
Ludovic Brenta.

Re: Ensuring postconditions in the face of exceptions

[cjpsimon]

On 15 mar, 10:14, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote:
> Alex Mentis wrote on comp.lang.ada:
>
> > Well, I'm not sure I'm suggesting you raise extra exceptions, just
> > handle them in the calling subprogram instead of the called
> > subprogram.  You're already re-raising the exception with the called
> > subprogram exception handler:
>
> 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.
>
> So let me summarize the various suggestions so far:
>
> (1) pass Dirty as "access" instead of "in out": works but, as you
> nicely put it, "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."
>
> (2) pass Dirty encapsulated in a limited record: also works but this
> is even worse (IMHO) than "access" because it obscures the purpose of
> the limited record type. I'd have to have 10 lines of comments just to
> explain why there is a limited record type containing a single Boolean
> component.
>
> (3) make Dirty part of the object type T: the flag is necessary in
> only one of the places where T is used; also T is serialized in
> several places, so changing it is not a good idea.
>
> (4) handle the exception in the caller: there is no longer a central
> place for handling the  Dirty flag therefore future maintenance is
> harder. As a side effect, the procedure Refresh loses most of its
> purpose, so might as well disappear.
>
> I came up with (5): place both Dirty and the Object to be visited in a
> record type and pass an access value to that record. This is a
> variation of (1); it is still ugly (IMHO) but the record type and the
> access-to-record type already existed so the change to the code base
> was minimal. Since, however, the existing record type contains many
> other things besides the Object and Dirty flag, the procedure Refresh
> receives much more information than it really needs, which might break
> encapsulation.
>
> All in all, no solution so far is as elegant as I would have liked but
> thanks anyway for the various suggestions. I think that (1) is still
> the least ugly though.
>
> --
> Ludovic Brenta.

Founded in ARM :

A type is a by-reference type if it is a descendant of one of the
following:
5    * a tagged type;
6    * a task or protected type;
7    * a nonprivate type with the reserved word limited in its
declaration;
8    * a composite type with a subcomponent of a by-reference type;
9    * a private type whose full type is a by-reference type.

May be a (6) option is to create a tagged type ?

Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

cjpsimon@gmail.com wrote on comp.lang.ada:
> On 15 mar, 10:14, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote:
>> (1) pass Dirty as "access" instead of "in out": works but, as you
>> nicely put it, "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."
>
>> (2) pass Dirty encapsulated in a limited record: also works but this
>> is even worse (IMHO) than "access" because it obscures the purpose of
>> the limited record type. I'd have to have 10 lines of comments just to
>> explain why there is a limited record type containing a single Boolean
>> component.
>
>> (3) make Dirty part of the object type T: the flag is necessary in
>> only one of the places where T is used; also T is serialized in
>> several places, so changing it is not a good idea.
>
>> (4) handle the exception in the caller: there is no longer a central
>> place for handling the  Dirty flag therefore future maintenance is
>> harder. As a side effect, the procedure Refresh loses most of its
>> purpose, so might as well disappear.
>
>> I came up with (5): place both Dirty and the Object to be visited in a
>> record type and pass an access value to that record. This is a
>> variation of (1); it is still ugly (IMHO) but the record type and the
>> access-to-record type already existed so the change to the code base
>> was minimal. Since, however, the existing record type contains many
>> other things besides the Object and Dirty flag, the procedure Refresh
>> receives much more information than it really needs, which might break
>> encapsulation.
[...]
> May be a (6) option is to create a tagged type ?

I see this as a variant of (2) and has the same drawbacks. In this
case I would have to explain why I use a tagged type that has no
primitive operations (the procedure Refresh does not have to be
primitive for this type) and no type extensions .

--
Ludovic Brenta.

Re: Ensuring postconditions in the face of exceptions

[J-P. Rosen]

Ludovic Brenta a �crit :

>> May be a (6) option is to create a tagged type ?
> 
> I see this as a variant of (2) and has the same drawbacks. In this
> case I would have to explain why I use a tagged type that has no
> primitive operations (the procedure Refresh does not have to be
> primitive for this type) and no type extensions .
> 
Proposal (7):

Make Dirty a (limited) private type -say Status- with functions Is_Dirty
and Is_Clean. You are then free to implement it as a by-reference type.

If it's a mess, hide it...

-- 
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr

Re: Ensuring postconditions in the face of exceptions

[Jeffrey R. Carter]

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?

-- 
Jeff Carter
"Have you gone berserk? Can't you see that that man is a ni?"
Blazing Saddles
38

Re: Ensuring postconditions in the face of exceptions

[Robert Matthews]

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

Re: Ensuring postconditions in the face of exceptions

[Robert A Duff]

Ludovic Brenta <ludovic@ludovic-brenta.org> writes:

> That's an interesting suggestion but we've patched the run-time library
> so that it dumps core on every exception;...

Then how can it ever get to the "when others" in Refresh?
Or do you mean it dumps core, and then the program continues
on past the point of the bug (propagates the exception,
handles it, etc)?

Is "dirty" a property of the object being visited?
If so, would it make sense to make it a component
of that object, and make sure that is passed by
reference (either by explicitly passing a pointer,
or by making the type limited or tagged)?

By the way, I think it makes perfect sense to have
different postconditions for normal return, and for
each exception that might be raised.

- Bob

Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

Robert A Duff wrote on comp.lang.ada:
> Ludovic Brenta <ludo...@ludovic-brenta.org> writes:
> > That's an interesting suggestion but we've patched the run-time library
> > so that it dumps core on every exception;...
>
> Then how can it ever get to the "when others" in Refresh?
> Or do you mean it dumps core, and then the program continues
> on past the point of the bug (propagates the exception,
> handles it, etc)?

Yes, that is correct.

> Is "dirty" a property of the object being visited?
> If so, would it make sense to make it a component
> of that object, and make sure that is passed by
> reference (either by explicitly passing a pointer,
> or by making the type limited or tagged)?

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.

> By the way, I think it makes perfect sense to have
> different postconditions for normal return, and for
> each exception that might be raised.

I agree; this generalizes my question even more.

--
Ludovic Brenta.

Re: Ensuring postconditions in the face of exceptions

[Robert A Duff]

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

Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

Robert A Duff wrote on comp.lang.ada:
> Ludovic Brenta <ludo...@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.

Yes, that's the solution I have, currently, i.e. (5); except that the
Cache type already existed before, has other unrelated components and
is not limited.

--
Ludovic Brenta.

Re: Ensuring postconditions in the face of exceptions

[Robert A Duff]

Ludovic Brenta <ludovic@ludovic-brenta.org> writes:

> Robert A Duff wrote on comp.lang.ada:
>> Ludovic Brenta <ludo...@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.
>
> Yes, that's the solution I have, currently, i.e. (5); except that the
> Cache type already existed before, has other unrelated components and
> is not limited.

Right, but you said you didn't like it, because of the "other unrelated
components".  So the type I'm suggesting above is a different one
than the existing one -- I'm suggesting this new type would NOT
have the unrelated components.

I haven't seen your code, of course, so I could be talking
complete nonsense.  ;-)

- Bob

Re: Ensuring postconditions in the face of exceptions

[Jeffrey R. Carter]

Ludovic Brenta wrote:
> 
> That's an interesting suggestion but we've patched the run-time library
> so that it dumps core on every exception; we use exceptions only for
> exceptional situations and dumping core freezes the system for 30
> seconds to produce a file roughly 300 MiB in size.  So I would rather
> not raise exceptions that are do not detect a bug.

Let me see if I understand this correctly: Visit raises an exception, which 
freezes the system for 30 s and writes a large file. Then you handle the 
exception, assign to Dirty, and re-raise the exception, again freezing the 
system and writing the file.

Is that how this is expected to work?

-- 
Jeff Carter
"We'll make Rock Ridge think it's a chicken
that got caught in a tractor's nuts!"
Blazing Saddles
87

Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta]

Jeffrey R. Carter wrote on comp.lang.ada:
> Ludovic Brenta wrote:
>
> > That's an interesting suggestion but we've patched the run-time library
> > so that it dumps core on every exception; we use exceptions only for
> > exceptional situations and dumping core freezes the system for 30
> > seconds to produce a file roughly 300 MiB in size.  So I would rather
> > not raise exceptions that are do not detect a bug.
>
> Let me see if I understand this correctly: Visit raises an exception, which
> freezes the system for 30 s and writes a large file. Then you handle the
> exception, assign to Dirty, and re-raise the exception, again freezing the
> system and writing the file.
>
> Is that how this is expected to work?

Not exactly because we've taken this situation into account when
patching the run-time library. It dumps core on the first exception
but not on re-raises, so re-raises are OK.

--
Ludovic Brenta.

Re: Ensuring postconditions in the face of exceptions

[AdaMagica]

> 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).