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.7 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM,REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,1d1caf8fb79ff030 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.202.168 with SMTP id kj8mr8982814pbc.1.1332684863524; Sun, 25 Mar 2012 07:14:23 -0700 (PDT) Path: kz5ni32400pbc.0!nntp.google.com!news2.google.com!news4.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.139.MISMATCH!xlned.com!feeder7.xlned.com!news2.euro.net!multikabel.net!newsfeed20.multikabel.net!zen.net.uk!dedekind.zen.co.uk!reader02.nrc01.news.zen.net.uk.POSTED!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK loop VCs that go "one beyond" the loop? Date: Sun, 25 Mar 2012 15:14:23 +0100 Message-ID: References: Reply-To: phil.jpthornley@gmail.com MIME-Version: 1.0 User-Agent: MicroPlanet-Gravity/3.0.4 Organization: Zen Internet NNTP-Posting-Host: 69092d4c.news.zen.co.uk X-Trace: DXC=>1N;_PEn\Dcko]em;Y=Pd`]G;bfYi23hd=dR0\ckLKG`WeZ<[7LZNRf]1l8n3?C7K`6JNOYoB;SJn?_^gSgIg3DaIELE81;m[1o X-Complaints-To: abuse@zen.co.uk Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-03-25T15:14:23+01:00 List-Id: In article , PChapin@vtc.vsc.edu says... > Thanks for your comments. They are helpful, as always. The problem I'm > having, in general (no longer related to any specific VC), is that if > the loop assertion mentions the loop index variable there is a tendency > for SPARK to generate an unprovable VC of the form > > Hx: loop__1__i <= some_array__index__subtype__1__last > ... > Cy: loop__1__i + 1 <= some_array__index__subtype__1__last > > This is for the path from the assertion to the assertion and it's trying > to show that the loop index variable is always in bounds of some > array... even *after* the last iteration. This generally isn't true, but > it doesn't matter because there is no "next" iteration in that case. > > If I write a loop assertion that doesn't mention the loop index variable > this problem doesn't arise, naturally. However, I can avoid it anyway by > doing... something... with that loop assertion. My problem is that I > haven't quite figured out what triggers VCs like the one above so I have > to kind of guess my way around how to avoid them. I don't believe that the Examiner generates a path *to* the loop iteration for the last iteration - I can only imagine that there is something you are not seeing. It's quite true that any VC that references the loop index will have your Hx above - because the loop index is within the bounds of its subtype at the start of the path. However, for all paths from the assertion to the assertion, the Examiner will certainly generate a hypothesis that the loop index is strictly less than the final value of the loop range (assuming absence of 'reverse' of course). Therefore you have to look at what you know about the relative values of the last loop index value and 'Last of the array index subtype. This is one part of what was required for the code in in your original post (Event_Array(I).Description_Size <= Description'Length) and you provided the other part. This undoubtedly gets more involved when the last loop index value is an expression referencing one or more variables, but this shouldn't make any fundamental difference. (In this case it's sometimes helpful to temporarily introduce a local variable for the upper bound of the loop range.) Cheers, Phil