--- layout: fc_discuss_archives title: Message 98 from Frama-C-discuss on October 2013 ---
Hello, Le jeu. 31 oct. 2013 09:49:13 CET, Alessio Iotti <alle.iot at gmail.com> a ?crit : > the attached file is a simple C program that (perhaps) computes the > greatest common divisor > of two integers. > I have defined a predicate, IsGCD(a, b, val), that is true if val is > the GCD of a and b. > Frama-C can prove the loop invariant and variant, but cannot prove the > ensures clause of the contract: I don't understand why. First, your Divides and IsGCD predicates do not need to take a label as parameter: this is only needed for predicates that access C memory (e.g. use the value of a global variable and/or dereference some pointer), which is not the case here: you express a property about the mathematical integer that are given as argument. You might also want to add some positivity conditions in the definition of IsGCD Second, the last part of your loop invariant: \forall integer z ; (IsGCD{Here}(a, b, z)) ==> (IsGCD{Pre}(a, b, z)) is a tautology: since Here and Pre are irrelevant, it amounts to \forall z; P(z) ==> P(z). It is thus completely useless in proving the ensures. 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). Best regards, -- E tutto per oggi, a la prossima volta. Virgile