Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] wp loop invariant problem

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