Processing array subsections, a newbie question.
in [ADA]
|
From: Niklas Holsti on 13 Jun 2010 02:28 Ludovic Brenta wrote: > "Peter C. Chapin" <pcc482719(a)gmail.com> writes: >> Ok : Boolean := True; >> Index_Fst : Natural := Buffer'First; >> Index_Lst : Natural; >> ... >> >> while Ok and Index_Fst <= Buffer'Last loop >> Do_Something(Buffer, Index_Fst, Index_Lst, Ok); >> Index_Fst := Index_Lst + 1; >> end loop; >> >> The problem with this code is that the assignment to Index_Fst inside the loop >> might raise Constraint_Error if Index_Lst = Buffer'Last after Do_Something >> finishes. I can work around this problem but my solutions tend to be rather >> ungainly looking. Surely there must be an easy way to handle this. Constraint_Error would be raised only if Index_Lst = Natural'Last after Do_Something. By subtyping the index type of Buffer you could ensure that Buffer'Last < Natural'Last, which would avoid the risk of Constraint_Error. (Perhaps this is the ungainly work-around that you mention.) > How about: A few nitpicks on Ludovic's suggestion: > Ok : Boolean := True; The initial value for Ok is unneccessary, as Do_Something will assign Ok before it it used. > Index_Fst : Natural := Buffer'First; > Index_Lst : Natural; > ... > loop > Do_Something(Buffer, Index_Fst, Index_Lst, Ok); In this call of Do_Something, Index_Fst may not be a valid index for Buffer, since there is no preceding check that Index_Fst <= Buffer'Last, as there was in the original while-loop. But perhaps it is known, in the original context, that Buffer is not empty. > exit when not Ok; > exit when Index_Fst = Buffer'Last; For robustness I would write Index_Fst >= Buffer'Last. (Perhaps this could also help some SPARK range analysis.) > Index_Fst := Index_Lst + 1; > end loop; So my suggestion is: Ok : Boolean; Index_Fst : Natural := Buffer'First; Index_Lst : Natural; .... if Index_Fst <= Buffer'Last then -- Buffer is not empty, something to be done. loop Do_Something(Buffer, Index_Fst, Index_Lst, Ok); exit when not Ok; exit when Index_Fst >= Buffer'Last; Index_Fst := Index_Lst + 1; end loop; else -- Buffer is empty. ... end if; -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .
From: Stephen Leake on 13 Jun 2010 07:00 "Peter C. Chapin" <pcc482719(a)gmail.com> writes: > procedure Do_Something > (Buffer : in Buffer_Type; > Fst : in Natural; > Lst : out Natural; > Ok : out Boolean); Change this to: procedure Do_Something (Buffer : in Buffer_Type; Last : in out Natural; Ok : out Boolean); -- Operate on Buffer (Last + 1 ..), update Last to last item operated -- on. -- -- Stephe
From: Simon Wright on 13 Jun 2010 07:04 Stephen Leake <stephen_leake(a)stephe-leake.org> writes: > "Peter C. Chapin" <pcc482719(a)gmail.com> writes: > >> procedure Do_Something >> (Buffer : in Buffer_Type; >> Fst : in Natural; >> Lst : out Natural; >> Ok : out Boolean); > > Change this to: > > procedure Do_Something > (Buffer : in Buffer_Type; > Last : in out Natural; > Ok : out Boolean); > > -- Operate on Buffer (Last + 1 ..), update Last to last item operated > -- on. What would happen if Buffer'First was Natural'First?
From: Peter C. Chapin on 13 Jun 2010 10:01 Gene wrote: > Yes! Or save a line with > > loop > Do_Something(Buffer, Index_Fst, Index_Lst, Ok); > exit when not Ok or Index_Fst = Buffer'Last; > Index_Fst := Index_Lst + 1; > end loop; > > Loop exit (with optional naming, which obviates the problems of > 'break' in C and its successors) is one of the small beauties of Ada... Thanks for the suggestion (by you and others) for using a loop exit. SPARK has some restrictions on how 'exit' can be used; I'm not sure if they will apply to my case or not, but I can look into it. In my case there is also a state machine involved and the exiting would have to take place inside a case statement inside the loop. I seem to recall that SPARK has an issue with exiting from nested control structures but I can experiment. Peter
From: Peter C. Chapin on 13 Jun 2010 10:09
Niklas Holsti wrote: > Constraint_Error would be raised only if Index_Lst = Natural'Last after > Do_Something. By subtyping the index type of Buffer you could ensure > that Buffer'Last < Natural'Last, which would avoid the risk of > Constraint_Error. (Perhaps this is the ungainly work-around that you > mention.) In fact that is exactly what I'm doing now. I'm not sure if "ungainly" is the right word to use but my concern is that now I'm using a variable to index the array that has a subtype that can, in principle, extend outside of the array. I haven't yet tried to prove my program free of run time errors using SPARK but I anticipate that doing so will be harder than it might otherwise be because of this situation. My experience with SPARK so far is that it is very desirable to express precise intentions with one's subtypes. On the other hand the code fragment I showed before won't prove at all, of course, since it could in fact raise Constraint_Error. The early loop exit approach might be workable for me. I didn't really think of that. I might have to reorganize a few things, but I'm used to that! Thanks for the suggestion. Peter |