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.129.137.3 with SMTP id z3mr7849293ywf.20.1489770976366; Fri, 17 Mar 2017 10:16:16 -0700 (PDT) X-Received: by 10.157.31.39 with SMTP id x36mr890055otd.12.1489770976323; Fri, 17 Mar 2017 10:16:16 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!1.eu.feeder.erje.net!feeder.erje.net!2.us.feeder.erje.net!feeder.usenetexpress.com!feeder1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!n37no945968qtb.0!news-out.google.com!78ni17440itm.0!nntp.google.com!w124no3871901itb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 17 Mar 2017 10:16:15 -0700 (PDT) In-Reply-To: <4caef81d-b348-48e2-82df-bbc81491dbe4@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: <58caf52b$0$24793$426a74cc@news.free.fr> <2ac671c3-ea12-4a53-9ee8-dc72b9702bb2@googlegroups.com> <966f8f48-13c0-4928-9aad-624d2184418f@googlegroups.com> <4caef81d-b348-48e2-82df-bbc81491dbe4@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: [Spark] Proving GCD From: Phil Thornley Injection-Date: Fri, 17 Mar 2017 17:16:16 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:46412 Date: 2017-03-17T10:16:15-07:00 List-Id: On Friday, March 17, 2017 at 1:28:44 PM UTC, Fr=C3=A9d=C3=A9ric PRACA wrote= : > Le vendredi 17 mars 2017 14:24:48 UTC+1, Fr=C3=A9d=C3=A9ric PRACA a =C3= =A9crit=C2=A0: > > Le vendredi 17 mars 2017 14:00:54 UTC+1, Phil Thornley a =C3=A9crit=C2= =A0: > > > >=20 > > > > And I still have the same message from Spark. Any idea ? > > >=20 > > > Any non-trivial code with loops will need to have loop invariants. Th= ese links explain why and a bit about how to write them: > > > http://www.spark-2014.org/entries/detail/spark-2014-rationale-loop-in= variants > > > http://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-ho= w-to-write-loop-invariants > > There's already one but a really simple one, just stating that Local_B = is decreasing. >=20 > My mistake, there's no invariant only a variant :) > I will try to find one. >=20 > > I will check with the links you provided me. > >=20 > > > I would also recommend starting with an easier example than the GCD a= lgorithm. > A Google search for "SPARK loop invariant" will throw up lots m= ore examples. > > > (But some of these will be about the previous version of SPARK - now = referred > to as SPARK 2005.) > > As I own a copy of the "Building High Integrity Applications with SPARK= " book from John W. McCormick and Peter Chapin, I already have several exam= ples but I found it more interesting to take an example from scratch. > > Moreover, it was a good point to compare with the unit test method as s= een in http://www2.cs.uni-paderborn.de/cs/ag-schaefer-static/Lehre/Lehrvera= nstaltungen/Vorlesungen/SoftwareQualityAssurance/WS0405/SQA-III-p104-182.pd= f page 56. > >=20 > > > Note that your postcondition states that the result is a common divis= or of A > > > and B, but does not state that it is the greatest such divisor. > > But doing so would be to rewrite the whole algorithm in the contract, n= o ? > >=20 > > Fred Since there isn't any code after the loop, except the assignment to value, = a possible way to start finding an invariant is to 'hoist' the postconditio= n back into the end of the loop: pragma Loop_Invariant (A mod Local_A =3D 0=20 and B mod Local_A =3D 0=20 > and ((A > 0 and then Local_A <=3D A) OR (A =3D 0 and then Local_A =3D B)); This should guarantee that the postcondition is proved, and you might find = it easier to prove this invariant for the different paths. Cheers, Phil