--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on October 2015 ---
> Iâve been trying to get a working bubble sort implementation to verify using the latest frama-c and WP plugin. After failing for a few days, I tried narrowing my problems down to simpler tasks. The following code is supposed to(!) bubble up the maximum value of the array to the position a[end-1] of the array, but notice that I intentionally modified the code so that it doesnât change the array at all. Nevertheless, the WP plugin reports valid for all the proof goals, including the post-condition. Am I missing something obvious here? Yes ! Indeed, there is nothing about the preservation of the elements in the array across the function. Something like : /*@ ⦠ensures \forall integer i ; start <= i < end ==> \exists integer j ; start <= j < end ==> a[i] == \old( a[j] ) ; */ (and the other way). L.