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.157.56.155 with SMTP id p27mr6233332otc.124.1489743187743;
        Fri, 17 Mar 2017 02:33:07 -0700 (PDT)
X-Received: by 10.157.36.105 with SMTP id p96mr1529481ota.15.1489743187709;
 Fri, 17 Mar 2017 02:33:07 -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!u69no3750272ita.0!news-out.google.com!78ni17158itm.0!nntp.google.com!u69no3750262ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 17 Mar 2017 02:33:07 -0700 (PDT)
In-Reply-To: <58caf52b$0$24793$426a74cc@news.free.fr>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=90.115.177.251;
 posting-account=P04rJQoAAAAcZ1eXXrg_e5YPG0xhsQtg
NNTP-Posting-Host: 90.115.177.251
References: <58caf52b$0$24793$426a74cc@news.free.fr>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <eaf03e7d-a2dd-4490-9156-3a25c32634eb@googlegroups.com>
Subject: Re: [Spark] Proving GCD
From: =?UTF-8?B?RnLDqWTDqXJpYyBQUkFDQQ==?= <frederic.praca@free.fr>
Injection-Date: Fri, 17 Mar 2017 09:33:07 +0000
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Xref: news.eternal-september.org comp.lang.ada:46408
Date: 2017-03-17T02:33:07-07:00
List-Id: <comp.lang.ada>

Le jeudi 16 mars 2017 21:27:24 UTC+1, Fr=C3=A9d=C3=A9ric PRACA a =C3=A9crit=
=C2=A0:
> Hi guys,

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'res=
ult =3D B));

It was tested with the following code
Pragma SPARK_Mode;

with Ada.text_io; use Ada.text_io;
with GCD_Package; use GCD_Package;

procedure TestGCD is

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;

And I still have the same message from Spark. Any idea ?