Re: [Spark] Proving GCD

["Frédéric PRACA" <frederic.praca@free.fr>]

Le jeudi 16 mars 2017 21:27:24 UTC+1, Frédéric PRACA a écrit :
> Hi guys,

Here is the new version of the contract
function gcd (A : Natural; B : Positive) return Natural
     with
       Global => null,
       Depends => (gcd'Result => (A,B)),
       Post =>  A mod gcd'Result = 0 
       and B mod gcd'Result = 0 
       and ((A > 0 and then gcd'Result <= A) OR (A = 0 and then gcd'result = 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) = " & Integer'Image(gcd(a => 420,
                                                     b => 252)));
   
   Put_line ("GCD (512, 252) = " & Integer'Image(gcd(a => 512,
                                                     b => 252)));
   
   Put_line ("GCD (1, 1) = " & Integer'Image(gcd(a => 1,
                                                 b => 1)));
   
   Put_line ("GCD (0, 1) = " & Integer'Image(gcd(a => 0,
                                                 b => 1)));
end TestGCD;

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