--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on May 2010 ---
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? thanks, naghmeh > 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 -- Naghmeh Ghafari, Ph.D. Research Associate Critical Systems Labs, Inc. Tel: (604) 638 7393 Cell: (778) 994 4802