--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2010 ---
Hello, 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