--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on November 2013 ---
Le ven. 01 nov. 2013 16:11:05 CET, Alessio Iotti <alle.iot at gmail.com> a ?crit : > Excuse me, but I'm not sure I understand. When you say: > > > > I suspect that you wanted to write > > IsGCD(a,b,z) ==> IsGCD(\at(a,Pre),\at(b,Pre),z). > > However, I'm not completely sure that existing ATP will have much > > luck in proving IsGCD(a-b,b,z) ==> IsGCD(a,b,z). > > > > What you means is that, even if the correct loop invariant is: > IsGCD(a,b,z) ==> IsGCD(\at(a,Pre),\at(b,Pre),z) > the theorem prover is not able to prove it? Exactly. This new invariant indeed looks better, however most ATP have trouble with non-linear arithmetic formulas, such as x%y==0. The other point is that it might also not be obvious for an ATP that IsGCD(a,a,a) (which is the point that would allow to conclude that return a; indeed return the GCD). > If this is the case, there is something I can change in the IsGCD > predicate, apart > from the positivity conditions, to help the ATP in his proof or is it > better to change > the invariant? You can't really change the invariant. It might be possible to tweak the definition of Divides and/or isGCD (see for instance the definitions adopted for proving the implementation of a GCD function in Java at http://toccata.lri.fr/gallery/GcdJava.en.html), but more importantly, you'll probably have to guide the ATPs by providing intermediate lemmas about IsGCD that can then be used in the proof of the function itself. Best regards, -- E tutto per oggi, a la prossima volta. Virgile