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

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