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.5 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM,STOX_REPLY_TYPE autolearn=no autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!goblin3!goblin.stu.neva.ru!news.netfront.net!not-for-mail From: "Phil Thornley" Newsgroups: comp.lang.ada Subject: Re: Issue with SPARK 2014 Date: Sun, 18 Oct 2015 09:44:43 +0100 Organization: Netfront http://www.netfront.net/ Message-ID: References: <4187f92b-770a-4d76-85c0-14f2eba2dee8@googlegroups.com> <41a7f7f9-65b4-43a3-b817-f5d9c6a3d015@googlegroups.com> NNTP-Posting-Host: 88.97.49.112 Mime-Version: 1.0 Content-Type: text/plain; format=flowed; charset="iso-8859-1"; reply-type=original Content-Transfer-Encoding: 7bit X-Trace: adenine.netfront.net 1445157887 58289 88.97.49.112 (18 Oct 2015 08:44:47 GMT) X-Complaints-To: news@netfront.net NNTP-Posting-Date: Sun, 18 Oct 2015 08:44:47 +0000 (UTC) In-Reply-To: X-Priority: 3 X-MSMail-Priority: Normal Importance: Normal X-Newsreader: Microsoft Windows Live Mail 16.4.3528.331 X-MimeOLE: Produced By Microsoft MimeOLE V16.4.3528.331 X-Antivirus: avast! (VPS 151017-1, 17/10/2015), Outbound message X-Antivirus-Status: Clean Xref: news.eternal-september.org comp.lang.ada:27995 Date: 2015-10-18T09:44:43+01:00 List-Id: On Tuesday, 15 October 2015 18:28:39 UTC+1, Serge Robyns wrote: [snip] > When trying to build a small standalone body I gets proved successfully > with the below code. However the call is using constant values. > I'm wondering if the fact that here the prover has constants in the > procedure call makes it possible for him to prove it. No, the use of constants in the procedure call is irrelevant. > Now in essence the moves are either given by a player or selected by an > algorithm. I was expecting that SPARK could prove the procedure by using > the procedure signature, in worst case pre/post conditions. That's exactly what is done - the Evaluate_Board procedure is proved for all possible (valid) calls. > The essence I'm trying to state in the loop invariant (which I've put to > shut up other SPARK messages) is that the count will never exceed a > certain range. You can't have more "tiles" than there is space to put > them. Every loop has a loop invariant (it's needed to cut the code as Stuart explained). If you don't supply one the SPARK tools create a default one. The messages that you get without an explicit loop invariant are because the default loop invariant isn't strong enough for this code. > Now I play with this code from time to time when I've an urge to make it > proven or when I read about how nice spark is. [code snipped] I don't think that you need more than one Loop_Variant in any loop, this is only needed to prove termination of the loop and just one valid loop variant should be enough. Cheers, Phil --- This email has been checked for viruses by Avast antivirus software. https://www.avast.com/antivirus --- news://freenews.netfront.net/ - complaints: news@netfront.net ---