Re: [Spark] Proving GCD

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

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