--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on May 2010 ---
Hi, I am trying to verify a very simple bubble sort example, using jessie (Beryllium). My default solver is Alt-Ergo. I used HAVOC (and Z3) to verify this example, which was relatively straight forward. I am using similar loop invariants, but still there is a safety property 'variant decrease' that I can't verify. I think this is because of the While(true) loop I have for which I cannot come up with a proper strictly decreasing loop variant. I also cannot verify my post condition. I appreciate any suggestions or hint. In my version of jessie, I cannot use #pragma JessieTerminationPolicy (user). It is not recognized in my version. cheers, naghmeh #define TRUE 1 #define FALSE 0 /*@ requires size > 0; @ requires \valid(arr+ (0..size-1)); @ ensures \forall int i; 0 <= i <= size - 2 ==> arr[i] <= arr[i+1]; */ void bubble_sort(int *arr, int size) { while (TRUE) { int aux = 0; int i = 0; /*@ loop invariant 0 <= i && i <= size -1 ; @ loop variant size - i; @*/ while (i < size-1) { if (arr[i] > arr[i+1]) { int tmp = arr[i]; arr[i] = arr[i+1]; arr[i+1] = tmp; aux = i; } i++; } if (aux == 0) break; } }