Re: [Spark] Proving GCD

[Phil Thornley <phil.jpthornley@gmail.com>]

On Friday, March 17, 2017 at 9:33:08 AM UTC, Frédéric PRACA wrote:
> 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 ?

Any non-trivial code with loops will need to have loop invariants. These links explain why and a bit about how to write them:
http://www.spark-2014.org/entries/detail/spark-2014-rationale-loop-invariants
http://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-how-to-write-loop-invariants

I would also recommend starting with an easier example than the GCD algorithm. A Google search for "SPARK loop invariant" will throw up lots more examples. (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