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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA 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.235.4 with SMTP id ui4mr16181350pbc.3.1332673036670; Sun, 25 Mar 2012 03:57:16 -0700 (PDT) Path: kz5ni31878pbc.0!nntp.google.com!news2.google.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Sun, 25 Mar 2012 05:57:14 -0500 Date: Sun, 25 Mar 2012 06:57:05 -0400 From: "Peter C. Chapin" User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: SPARK loop VCs that go "one beyond" the loop? References: In-Reply-To: Message-ID: X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-BCTv0Plpud+RhFv7NHcHxw9gdKsv8dYsnx+SyFaBv5tySzjv6sooT1M5dpZp1jt+L/QcFkMKv16J2Q2!tDS3TPiqxcVQ0JDNly7IAAALhpS5HagvahlPKF6kMvRrCTweDtoTAdXX68eXGog= X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 3069 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2012-03-25T06:57:05-04:00 List-Id: On 2012-03-20 14:18, Phil Thornley wrote: > Peter, > > The clue to the fact that you needed to add I=I% is in the hypotheses. > > I put enough code around the code in your initial post to get the VC that > you also posted. > > Then, with the additional condition, there are two particular hypotheses: > H2: fld_description_size(element(event_array, [i]))<= > description__index__subtype__1__last . > H13: loop__2__j< fld_description_size(element(event_array, [ > i__entry__loop__2])) . > where the conclusion is: > C1: loop__2__j< description__index__subtype__1__last . > > so by including I=I% in the loop invariant (which becomes i=i__entry__loop__2 > in the VC) the conclusion is provable. 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. Peter