Ensuring postconditions in the face of exceptions
in [ADA]
|
From: Ludovic Brenta on 15 Mar 2010 04:54 Robert A Duff wrote on comp.lang.ada: > Ludovic Brenta <ludo...(a)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.
From: Ludovic Brenta on 15 Mar 2010 04:56 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.
From: Ludovic Brenta on 15 Mar 2010 05:14 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.
From: AdaMagica on 15 Mar 2010 07:04 > 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).
From: cjpsimon on 15 Mar 2010 07:05
On 15 mar, 10:14, Ludovic Brenta <ludo...(a)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 ? |