Ensuring postconditions in the face of exceptions
in [ADA]
|
From: Alex Mentis on 14 Mar 2010 10:05 On Mar 12, 4:13 am, Ludovic Brenta <ludo...(a)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
From: Ludovic Brenta on 14 Mar 2010 10:21 Alex Mentis writes: > On Mar 12, 4:13 am, Ludovic Brenta <ludo...(a)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.
From: Alex Mentis on 14 Mar 2010 11:12 On Mar 14, 10:21 am, Ludovic Brenta <ludo...(a)ludovic-brenta.org> wrote: > Alex Mentis writes: > > On Mar 12, 4:13 am, Ludovic Brenta <ludo...(a)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;
From: Robert A Duff on 14 Mar 2010 11:38 Ludovic Brenta <ludovic(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)? 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
From: Jeffrey R. Carter on 14 Mar 2010 14:57
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 |