--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on May 2010 ---
Naghmeh Ghafari wrote: > > Thanks for the pointer. I actually tried the example in the slides > with Frama-C and Alt-Ergo and CVC3 as solvers. I get 'unknown' and > 'timeouts' for 5 of the loop invariants, but I still get a green > bullet for the post-condition. Although the slides show that CVC3 can > verify all of the conditions, but they don't pass in the version I am > running (i.e. CVC3 2.2 ). I tried to do a sanity check by negating the > post-condition and I still get the green bullet for the > post-condition. That doesn't sound right, or am I missing something > obvious here? > 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 Unfortunately, I do not know any way to check if someone's specification is inconsistent. The mistake "\exists x; A ==> B" is indeed quite common. For some time, I tried to promote the JML syntax which allows to write "\forall x; A; B" for "\forall x; A ==> B" and "\exists x; A; B" for "\exists x; A && B" but I got no success among the ACSL designers. An argument against is that, as far as I know, there is no such syntactic sugar in proof assistants like Coq, Isabelle, PVS, etc. General speaking, checking inconsistency of user's specifications is something we would like to have: any suggestions welcome! - Claude > > > >> Pedro Pereira and Ulisses Costa, brilliant students with excellent >> taste in the choice of their personal projects, proved the correctness >> of a bubble sort algorithm a while back (including termination). >> Looking at their slides briefly, it seems that the difficult part was >> first finding the invariant for the outer loop (slide 28) and that >> once you had that, it became a little clearer in which direction to >> look for the variant. In their version, there was a program variable >> that expressed almost directly how much of the (end of the) array was >> sorted (that variable was named i in their program). >> >> In yours, there doesn't seem to be such a variable, but you can always >> add to the program a ghost variable and ghost statements to make the >> logic of the loop clearer. Then the loop invariant and variant would >> be expressed in function of this ghost variable. To make your version >> somewhat similar to theirs, the ghost variable would represent the >> number of iterations of the outer loop so far. >> >> http://www.slideshare.net/UlissesCosta/correct-sorting-with-framac >> >> Good luck, >> >> Pascal >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >> > wha >