Processing array subsections, a newbie question.
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 13 Jun 2010 11:48 Le Sun, 13 Jun 2010 16:01:20 +0200, Peter C. Chapin <pcc482719(a)gmail.com> a écrit: > I seem to recall that SPARK has an issue with > exiting from nested control structures but I can experiment. > > Peter You have to exit from one to an outer one. Ex. if Loop1 includes Loop2 which includes Loop3, you cannot âexit Loop1â from Loop3 (will look for the reference if needed). -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.
From: Phil Thornley on 13 Jun 2010 12:57 On 13 June, 15:01, "Peter C. Chapin" <pcc482...(a)gmail.com> wrote: [...] > 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. I don't think the state machine will make any difference, but you certainly can't exit an enclosing loop when in a case arm - you have to move the exit(s) to after the 'end case'. This is not usually too much of a problem, but in your code it forces the exit to come after the increment (assuming that this has to stay in the case arm). As you suggest elsewhere in this thread, it is a good idea to have subtype constraints as tight as possible. In the situation you describe I would define a type (to replace your use of Natural) that has one extra value at the end (for the Index_Fst variable). Then define the array index as a subtype that excludes that extra value. This should allow the increment to stay in the case arm, with the exit following after the case. (BTW, if you haven't tried it yet, you will find that using unconstrained arrays creates additional work when doing run-time checks as the VCs generated by any reference to an array element use the limits for that array object, not just the array index subtype). Cheers, Phil
From: Yannick Duchêne (Hibou57) on 13 Jun 2010 14:39 Le Sun, 13 Jun 2010 18:57:14 +0200, Phil Thornley <phil.jpthornley(a)gmail.com> a écrit: > In the situation you > describe I would define a type (to replace your use of Natural) that > has one extra value at the end I see what you mean, but ... Personal feeling: this looks like a trick, would not recommend it. To be short: types should not defined this way. Implementation should be adjusted to specification (a type is a part of a specification) and not the opposite, that is, to adapt specifications (types here) to an implementation. -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.
From: Peter C. Chapin on 13 Jun 2010 14:58 Phil Thornley wrote: > I don't think the state machine will make any difference, but you > certainly can't exit an enclosing loop when in a case arm - you have > to move the exit(s) to after the 'end case'. > > This is not usually too much of a problem, but in your code it forces > the exit to come after the increment (assuming that this has to stay > in the case arm). Yes that could be a problem for me. On the other hand *most* of the cases do the increment. With a little thought I might be able to make them all do the increment... and then factor that out of the case. > As you suggest elsewhere in this thread, it is a good idea to have > subtype constraints as tight as possible. In the situation you > describe I would define a type (to replace your use of Natural) that > has one extra value at the end (for the Index_Fst variable). Then > define the array index as a subtype that excludes that extra value. > This should allow the increment to stay in the case arm, with the exit > following after the case. That sounds like what I've got at the moment. Maybe I'll just end up sticking with that and see how it plays out. > (BTW, if you haven't tried it yet, you will find that using > unconstrained arrays creates additional work when doing run-time > checks as the VCs generated by any reference to an array element use > the limits for that array object, not just the array index subtype). I'll keep that in mind. I could probably defined a constrained array type instead. In my situation the array sizes should only vary between about 20 and 40 elements. I could probably just define the array to have 40 elements (or whatever I actually need... I'll have to check). My state machine just returns once it is satisfied so it will ignore the extra "junk" if there is any. I think that would be okay. Thanks for your input. Peter
From: Phil Thornley on 13 Jun 2010 15:04
On 13 June, 19:39, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > Le Sun, 13 Jun 2010 18:57:14 +0200, Phil Thornley > <phil.jpthorn...(a)gmail.com> a écrit:> In the situation you > > describe I would define a type (to replace your use of Natural) that > > has one extra value at the end > > I see what you mean, but ... > Personal feeling: this looks like a trick, would not recommend it. To be > short: types should not defined this way. Implementation should be > adjusted to specification (a type is a part of a specification) and not > the opposite, that is, to adapt specifications (types here) to an > implementation. > That's quite a severe point of view - I would classify the extra value as a 'boundary value' as described in AQ&S 5.3.1 on subtypes. Cheers, Phil |