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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.182.213.73 with SMTP id nq9mr6629908obc.33.1444898677903; Thu, 15 Oct 2015 01:44:37 -0700 (PDT) X-Received: by 10.182.165.136 with SMTP id yy8mr79451obb.18.1444898677880; Thu, 15 Oct 2015 01:44:37 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!kq10no18692972igb.0!news-out.google.com!n2ni30768igy.0!nntp.google.com!kq10no18692965igb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 15 Oct 2015 01:44:37 -0700 (PDT) In-Reply-To: <4187f92b-770a-4d76-85c0-14f2eba2dee8@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=88.97.49.112; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q NNTP-Posting-Host: 88.97.49.112 References: <4187f92b-770a-4d76-85c0-14f2eba2dee8@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <41a7f7f9-65b4-43a3-b817-f5d9c6a3d015@googlegroups.com> Subject: Re: Issue with SPARK 2014 From: Phil Thornley Injection-Date: Thu, 15 Oct 2015 08:44:37 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:27980 Date: 2015-10-15T01:44:37-07:00 List-Id: On Wednesday, 14 October 2015 21:04:52 UTC+1, Stuart wrote: > On Tuesday, 13 October 2015 18:37:08 UTC+1, Serge Robyns wrote: > > I'm trying to use SPARK on a little game, so far only one error remains= and I've no clue on how to fix this. I've been trying various approaches. > > Here is the code snippet (hopefully complete enough). > ... > > medium: loop invariant might fail after first iteration, requires Count= 1 <=3D Columns'pred - 1 > > medium: loop invariant might fail after first iteration, requires Count= 2 < Number_Of_Columns >=20 > It has been a while (and a few versions of SPARK) since I played with thi= s, but I think the problem is that your loop invariants are not strong enou= gh - they don't carry enough information around the loop. >=20 > IIRC the loop invariant acts as a cut point, and it is only information i= n the invariant that is carried around the loop, earlier knowledge derived = from the modelling of the code and the pre-conditions is lost (unless it is= embedded in the loop invariant). >=20 > In your first case the only knowledge carried around the loop is that: > Count1 was <=3D Integer (Columns'Pred (Column) - Columns'First) > and you incremented it. >=20 > Consequently, at the next iteration SPARK warns you that the Invariant mi= ght fail, because if it was equal to Integer (Columns'Pred (Column) - Colu= mns'First) before, it will now (because of the increment) be greater!! >=20 > Unfortunately I do not have access to a copy of SPARK or the manuals here= to help you resolve it (I expect an expert will be along in a while), but = I would guess that you need to strengthen the invariant to an equality stat= ement that remains true. Stuart's explanation is quite correct. In the first version try changing the bound on Count1 to: Integer (Columns'Pred (Column) - J) so that it starts at 0 and increments by 1 on each loop. (and next time put up compilable code). Cheers, Phil