Ensuring postconditions in the face of exceptions
in [ADA]
|
From: Randy Brukardt on 12 Mar 2010 22:15 "Jeffrey R. Carter" <spam.jrcarter.not(a)spam.acm.org> wrote in message news:hndhls$3ns$1(a)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.
From: Stephen Leake on 13 Mar 2010 02:54 Ludovic Brenta <ludovic(a)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
From: Robert A Duff on 13 Mar 2010 10:14 "Randy Brukardt" <randy(a)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
From: Jeffrey R. Carter on 13 Mar 2010 12:34 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
From: Georg Bauhaus on 13 Mar 2010 14:33
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. |