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] Problem to Prove bubblesort

  • Subject: [Frama-c-discuss] Problem to Prove bubblesort
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Fri, 24 Apr 2009 08:58:51 +0200
 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