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.99.110.1 with SMTP id j1mr7964620pgc.52.1489755652156; Fri, 17 Mar 2017 06:00:52 -0700 (PDT) X-Received: by 10.157.3.54 with SMTP id 51mr1606739otv.20.1489755652104; Fri, 17 Mar 2017 06:00:52 -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!news.glorb.com!w124no3807110itb.0!news-out.google.com!m191ni1311itc.0!nntp.google.com!w124no3807105itb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 17 Mar 2017 06:00:51 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=88.97.25.230; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q NNTP-Posting-Host: 88.97.25.230 References: <58caf52b$0$24793$426a74cc@news.free.fr> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <2ac671c3-ea12-4a53-9ee8-dc72b9702bb2@googlegroups.com> Subject: Re: [Spark] Proving GCD From: Phil Thornley Injection-Date: Fri, 17 Mar 2017 13:00:52 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:46409 Date: 2017-03-17T06:00:51-07:00 List-Id: On Friday, March 17, 2017 at 9:33:08 AM UTC, Fr=C3=A9d=C3=A9ric PRACA wrote= : > Le jeudi 16 mars 2017 21:27:24 UTC+1, Fr=C3=A9d=C3=A9ric PRACA a =C3=A9cr= it=C2=A0: > > Hi guys, >=20 > Here is the new version of the contract > function gcd (A : Natural; B : Positive) return Natural > with > Global =3D> null, > Depends =3D> (gcd'Result =3D> (A,B)), > Post =3D> A mod gcd'Result =3D 0=20 > and B mod gcd'Result =3D 0=20 > and ((A > 0 and then gcd'Result <=3D A) OR (A =3D 0 and then gcd'r= esult =3D B)); >=20 > It was tested with the following code > Pragma SPARK_Mode; >=20 > with Ada.text_io; use Ada.text_io; > with GCD_Package; use GCD_Package; >=20 > procedure TestGCD is >=20 > begin > Put_line ("GCD (420, 252) =3D " & Integer'Image(gcd(a =3D> 420, > b =3D> 252))); > =20 > Put_line ("GCD (512, 252) =3D " & Integer'Image(gcd(a =3D> 512, > b =3D> 252))); > =20 > Put_line ("GCD (1, 1) =3D " & Integer'Image(gcd(a =3D> 1, > b =3D> 1))); > =20 > Put_line ("GCD (0, 1) =3D " & Integer'Image(gcd(a =3D> 0, > b =3D> 1))); > end TestGCD; >=20 > And I still have the same message from Spark. Any idea ? Any non-trivial code with loops will need to have loop invariants. These li= nks explain why and a bit about how to write them: http://www.spark-2014.org/entries/detail/spark-2014-rationale-loop-invarian= ts http://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-how-to-w= rite-loop-invariants I would also recommend starting with an easier example than the GCD algorit= hm. A Google search for "SPARK loop invariant" will throw up lots more exam= ples. (But some of these will be about the previous version of SPARK - now = referred to as SPARK 2005.) Note that your postcondition states that the result is a common divisor of = A and B, but does not state that it is the greatest such divisor. Cheers, Phil