--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with ensures



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