--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on May 2010 ---
> I did not know about these slides. I had a look at them, and can find an > obvious mistake in the post-condition they give: > > ?\forall integer a; ... ==> \exists integer b; 0 <= b < tam ==> ... > > The second "==>" should have been "&&" of course I just found another very common mistake in the bubble sort from the slides. For the outer loop: /*@ loop invariant 0 <= i < tam ; ... */ for (i=0; i<tam; i++) The loop invariant must hold for all iterations, including the last one where the exit condition becomes true. In general (for loops that terminate), the invariant should not be incompatible with the exit condition: the conjunction of these two properties holds when exiting the loop. So CVC3 should not be blamed for proving a post-condition and its negation in that example, because it indeed had "false" in its hypotheses (the outer loop invariant said that the loop didn't terminate). CVC3 should, instead, be blamed for having proved that the invariant held for the outer loop, which was *incorrect*. I will post a modified version of the Pereira-Costa version as soon as I am done playing with it and making adjustments. Another interesting tidbit is that Jessie is (probably rightly so) worried about integer overflows. Requiring an upper bound for tam seem to help prove some sub-properties. Pascal