--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem to Prove bubblesort



 Hello, I have a bubble_sort algorithm i want to prove.

I have added a lot of loop invariants and assertions,

but the provers fail to complete

The function:


 /*@
 predicate sorted_array{Here}(int* a, integer start_index, integer end_index) =
   \forall integer k1, k2;
    start_index <= k1 <= k2 <= end_index ==> a[k1] <= a[k2];
*/


/*@
 predicate all_smaller_than_the_last {Here}(int* a, integer start_index, integer end_index) =
   \forall integer k1;
    start_index <= k1 < end_index ==> a[k1] <= a[end_index];
*/



//use of swap funktion causes ERROR
 
/*@
 requires 0 < length;
 requires \valid_range(a, 0, length-1);
 ensures sorted_array(a, 0, length-1);
*/
void bubble_sort(int* a, int length) 
{

 
 int auf = 1;
 int ab;
 int fixed_auf = auf;

 /*@
  loop invariant fixed_auf == auf;
  loop invariant 0 < auf <= length; 
  loop invariant all_smaller_than_the_last(a, 0, auf-1);
  loop invariant sorted_array(a, 0, auf-1);
  loop invariant \forall integer k; auf < k < length ==> a[k] == \at(a[k], Pre);
 */
 for (; auf < length; auf++, fixed_auf = auf)   
 {   
  //@ assert sorted_array(a, 0, auf-1);    //IMPORTANT
  fixed_auf = auf;
  ab=auf; 
  //@ assert sorted_array(a, ab, auf); 
  /*@
   loop invariant fixed_auf == auf;
   loop invariant 0 <= ab <= auf;
   loop invariant all_smaller_than_the_last(a, 0, auf-1);
   loop invariant sorted_array(a, 0, ab-1);
   loop invariant sorted_array(a, ab, auf);
  
   loop invariant \forall integer k; auf < k < length ==> a[k] == \at(a[k], Pre);
  */    
  while (0 < ab && a[ab] < a[ab-1])
  {    
    //@ assert sorted_array(a, 0, ab-1);   //IMPORTANT
    //@ assert sorted_array(a, ab, auf);   //IMPORTANT
    
    
    //@ assert a[ab] < a[ab-1];        //IMPORTANT
    //@ assert a[ab] <= a[auf];
     
     int temp = a[ab]; 
    a[ab] = a[ab-1];                
    a[ab-1] = temp; 
   
   
    //@ assert a[ab-1] <= a[ab];        //IMPORTANT
    // not completely correct (actually  <), because only swapped when a[ab] < a[ab-1], 
   
        
    //@ assert sorted_array(a, ab+1, auf); // OK
 
   //@ assert  a[ab] <= a[auf];  
   //Problem: should be correct but is not proven
   //Solved: is proven due to predicate "all_smaller_than_the_last"
 
   //@ assert sorted_array(a, 0, ab-2); //ok //IMPORTANT
   
   //@ assert ab < auf ==> all_smaller_than_the_last(a, ab, ab+1);
   // NEEDS TO BE PROVEN   
      
   //@ assert  a[ab] <= a[auf];
   // NEEDS TO BE PROVEN  
   //@ assert sorted_array(a, ab, auf); // FAILURE
   
   // ==>   
   //@ assert sorted_array(a, ab-1, auf);  //IMPORTANT

   ab = ab-1;                 
   //@ assert sorted_array(a, 0, ab-1);   //IMPORTANT 
   //@ assert sorted_array(a, ab, auf);   //IMPORTANT
  }
  //@ assert sorted_array(a, 0, auf);     //IMPORTANT
 }
} 


Every assertion marked with " //IMPORTANT" should be proven.

I would like to know whether the next release, e.g., your development version suceeds to prove.

By the way, it is not possible to use the swap_function, this would cause an ERROR.


Sincerely

Christoph Weber
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090424/ad0b9020/attachment.htm