* [Spark] Proving GCD
@ 2017-03-16 20:27 Frédéric Praca
2017-03-17 9:33 ` Frédéric PRACA
0 siblings, 1 reply; 10+ messages in thread
From: Frédéric Praca @ 2017-03-16 20:27 UTC (permalink / raw)
Hi guys,
^ permalink raw reply [flat|nested] 10+ messages in thread
* [Spark] Proving GCD
@ 2017-03-16 20:31 Frédéric Praca
2017-03-17 1:20 ` Brian Kolden
2017-04-05 23:52 ` moy
0 siblings, 2 replies; 10+ messages in thread
From: Frédéric Praca @ 2017-03-16 20:31 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* [Spark] Proving GCD
2017-03-16 20:31 Frédéric Praca
@ 2017-03-17 1:20 ` Brian Kolden
2017-03-17 9:07 ` Frédéric PRACA
2017-04-05 23:52 ` moy
1 sibling, 1 reply; 10+ messages in thread
From: Brian Kolden @ 2017-03-17 1:20 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Proving GCD
2017-03-17 1:20 ` Brian Kolden
@ 2017-03-17 9:07 ` Frédéric PRACA
0 siblings, 0 replies; 10+ messages in thread
From: Frédéric PRACA @ 2017-03-17 9:07 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Proving GCD
2017-03-16 20:27 [Spark] Proving GCD Frédéric Praca
@ 2017-03-17 9:33 ` Frédéric PRACA
2017-03-17 13:00 ` Phil Thornley
0 siblings, 1 reply; 10+ messages in thread
From: Frédéric PRACA @ 2017-03-17 9:33 UTC (permalink / raw)
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 ?
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Proving GCD
2017-03-17 9:33 ` Frédéric PRACA
@ 2017-03-17 13:00 ` Phil Thornley
2017-03-17 13:24 ` Frédéric PRACA
0 siblings, 1 reply; 10+ messages in thread
From: Phil Thornley @ 2017-03-17 13:00 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Proving GCD
2017-03-17 13:00 ` Phil Thornley
@ 2017-03-17 13:24 ` Frédéric PRACA
2017-03-17 13:28 ` Frédéric PRACA
0 siblings, 1 reply; 10+ messages in thread
From: Frédéric PRACA @ 2017-03-17 13:24 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Proving GCD
2017-03-17 13:24 ` Frédéric PRACA
@ 2017-03-17 13:28 ` Frédéric PRACA
2017-03-17 17:16 ` Phil Thornley
0 siblings, 1 reply; 10+ messages in thread
From: Frédéric PRACA @ 2017-03-17 13:28 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Proving GCD
2017-03-17 13:28 ` Frédéric PRACA
@ 2017-03-17 17:16 ` Phil Thornley
0 siblings, 0 replies; 10+ messages in thread
From: Phil Thornley @ 2017-03-17 17:16 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Proving GCD
2017-03-16 20:31 Frédéric Praca
2017-03-17 1:20 ` Brian Kolden
@ 2017-04-05 23:52 ` moy
1 sibling, 0 replies; 10+ messages in thread
From: moy @ 2017-04-05 23:52 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2017-04-05 23:52 UTC | newest]
Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-03-16 20:27 [Spark] Proving GCD Frédéric Praca
2017-03-17 9:33 ` Frédéric PRACA
2017-03-17 13:00 ` Phil Thornley
2017-03-17 13:24 ` Frédéric PRACA
2017-03-17 13:28 ` Frédéric PRACA
2017-03-17 17:16 ` Phil Thornley
-- strict thread matches above, loose matches on Subject: below --
2017-03-16 20:31 Frédéric Praca
2017-03-17 1:20 ` Brian Kolden
2017-03-17 9:07 ` Frédéric PRACA
2017-04-05 23:52 ` moy
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox