From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,da5197b9dca0ed40 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!z10g2000yqb.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: Processing array subsections, a newbie question. Date: Sun, 13 Jun 2010 09:57:14 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <4c13db30$0$2391$4d3efbfe@news.sover.net> <8739wsottd.fsf@ludovic-brenta.org> <9e1f3f35-6f49-468f-be89-46d4f51f8193@f17g2000vbl.googlegroups.com> <4c14e3fd$0$2382$4d3efbfe@news.sover.net> NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: posting.google.com 1276448234 6628 127.0.0.1 (13 Jun 2010 16:57:14 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 13 Jun 2010 16:57:14 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: z10g2000yqb.googlegroups.com; posting-host=80.177.171.182; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:12650 Date: 2010-06-13T09:57:14-07:00 List-Id: On 13 June, 15:01, "Peter C. Chapin" 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