--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on June 2011 ---
Hello, Le mer. 29 juin 2011 10:14:49 CEST, mars Gu <marsishandsome at gmail.com> a ?crit : > > But in the file "max_element2.c", in Line 47, > I replace "loop invariant !(\exists integer k; 0 <= k < i && (a[max] < > a[k]));" > with "loop invariant IsMaximum(a, i, max);" which are the same. > But in this case, Frama-C can not prove. > Thanks for this report. As a matter of fact, the issue doesn't lie in the WP plugin per se, but in its interaction with alt-ergo (in particular Simplify can discharge the proof obligation). It seems like alt-ergo does not take advantage of the definition of the IsMaximum. The alt-ergo output can be tweaked to give the prover some hints (aka triggers) on how to use it. We will look into that. > > And also in the file "max_element3.c", > Line 55 can be proved while Line 44 can not. > The only difference between Line55 and Line44 is, that > Line 44 is a loop invariant, while Line 55 is an assersion. > There is another major difference in the hypotheses that you have in both cases. The assertion is expressed at the beginning of the loop body, which means in a state where by definition you know that the loop invariants hold, including the one which is exactly the same formula as the assertion. In other means, the prover must prove something like (A(s) && B(s)) ==> A(s), which is not that complicated. On the other hand, when attempting to prove that the corresponding loop invariant holds after one loop step, there is no such hypothesis: the assertion says something about the state at the beginning of the step, and we are trying to prove something about the state at the end of the step: this time we must prove something like A(s1) ==> [relation between s1 and s2] ==> A(s2) which is more complicated, and in fact rely on the definition of A (hence of IsMaximum in this particular case). Thus, it not that surprising that you can prove the former and not the latter Hope this helps, -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98