Re: [Spark] Proving GCD

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

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