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] question about a simple example and jessie

> 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