--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about a simple example and jessie



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;
   }
}