[Spark] Proving GCD

[Spark] Proving GCD

[Frédéric Praca]

Hi guys,

Re: [Spark] Proving GCD

[Frédéric PRACA]

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 ?

Re: [Spark] Proving GCD

[Phil Thornley]

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

Re: [Spark] Proving GCD

[Frédéric PRACA]

Le vendredi 17 mars 2017 14:00:54 UTC+1, Phil Thornley a écrit :
> > 
> > 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
There's already one but a really simple one, just stating that Local_B is decreasing.
I will check with the links you provided me.

> 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.)
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 examples 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 seen in http://www2.cs.uni-paderborn.de/cs/ag-schaefer-static/Lehre/Lehrveranstaltungen/Vorlesungen/SoftwareQualityAssurance/WS0405/SQA-III-p104-182.pdf page 56.

> 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.
But doing so would be to rewrite the whole algorithm in the contract, no ?

Fred

Re: [Spark] Proving GCD

[Frédéric PRACA]

Le vendredi 17 mars 2017 14:24:48 UTC+1, Frédéric PRACA a écrit :
> Le vendredi 17 mars 2017 14:00:54 UTC+1, Phil Thornley a écrit :
> > > 
> > > 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
> There's already one but a really simple one, just stating that Local_B is decreasing.

My mistake, there's no invariant only a variant :)
I will try to find one.

> I will check with the links you provided me.
> 
> > 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.)
> 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 examples 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 seen in http://www2.cs.uni-paderborn.de/cs/ag-schaefer-static/Lehre/Lehrveranstaltungen/Vorlesungen/SoftwareQualityAssurance/WS0405/SQA-III-p104-182.pdf page 56.
> 
> > 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.
> But doing so would be to rewrite the whole algorithm in the contract, no ?
> 
> Fred

Re: [Spark] Proving GCD

[Phil Thornley]

On Friday, March 17, 2017 at 1:28:44 PM UTC, Frédéric PRACA wrote:
> Le vendredi 17 mars 2017 14:24:48 UTC+1, Frédéric PRACA a écrit :
> > Le vendredi 17 mars 2017 14:00:54 UTC+1, Phil Thornley a écrit :
> > > > 
> > > > 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
> > There's already one but a really simple one, just stating that Local_B is decreasing.
> 
> My mistake, there's no invariant only a variant :)
> I will try to find one.
> 
> > I will check with the links you provided me.
> > 
> > > 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.)
> > 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 examples 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 seen in http://www2.cs.uni-paderborn.de/cs/ag-schaefer-static/Lehre/Lehrveranstaltungen/Vorlesungen/SoftwareQualityAssurance/WS0405/SQA-III-p104-182.pdf page 56.
> > 
> > > 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.
> > But doing so would be to rewrite the whole algorithm in the contract, no ?
> > 
> > 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 postcondition back into the end of the loop:
pragma Loop_Invariant (A mod Local_A = 0 
                   and B mod Local_A = 0 
>                  and ((A > 0 and then Local_A <= A)
                        OR
                        (A = 0 and then Local_A = 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

[Spark] Proving GCD

[Frédéric Praca]

Hi guys,
sorry for the first message, I clicked on the wrong button :D

I'm trying to train myself on Spark and I tried to see if a simple 
function like GCD could be proved.

I created the following :

GCD_Package is

   pragma SPARK_Mode;
   pragma Assertion_Policy(Check);
   
   function gcd (A : Natural; B : Positive) return Natural
     with
       Global => null,
       Depends => (gcd'Result => (A,B)),
       Post => gcd'Result <= A and A mod gcd'Result = 0 and B mod
       gcd'Result = 0 ;

end GCD_Package;

package body GCD_Package is

   pragma SPARK_Mode;

   function gcd (A : Natural; B : Positive) return Natural is
      Value : Natural;
      Temp : Natural; Local_B : Natural := B;
      Local_A : Natural := A;
   begin
      if A = 0 then
         value := B;
      else
         while Local_B > 0 loop
            pragma Loop_Variant (Decreases => Local_B);
            Temp := Local_B;
            Local_B := Local_A mod Local_B;
            Local_A := Temp;
         end loop;
         value := Local_A;
      end if;
      
      return value;
   end Gcd;

end GCD_Package;

The answer is always "postcondition might fail" and I don't know what to 
do. 
Do you have an idea on how to discharge all VCs and thus prove this code ?

Thanks
Fred

[Spark] Proving GCD

[Brian Kolden]

The gcd'Result <= A will fail if A = 0 and B = 1, I think. I can't verify that at the moment, but I'm fairly confident it will be false.

Re: [Spark] Proving GCD

[Frédéric PRACA]

Le vendredi 17 mars 2017 02:20:43 UTC+1, Brian Kolden a écrit :
> The gcd'Result <= A will fail if A = 0 and B = 1, I think. I can't verify that at the moment, but I'm fairly confident it will be false.

Arf !! You're right, this one is obviously wrong but even if I remove this part of the post conditon, I get the same message.

Re: [Spark] Proving GCD

[moy]

Hi Fred,

I had proved various versions of GCD some time ago, and needed some motivation to write a blog post about it. Your question gave me the impulse! Here is the blog post, that should answer your question: 

http://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-proving-the-ghost-common-denominator-gcd

Cheers