Wiki Agenda Contact Version française

Insertion Sort, C version

Sorting an array of integers in increasing order, by iterative insertion of the next element


Authors: Claude Marché

Topics: Array Data Structure / Sorting Algorithms

Tools: Frama-C / Jessie

See also: Selection Sort, C version

see also the index (by topic, by tool, by reference, by year)


The annotated code is as follows. First a predicate is declared to model what means being sorted in increasing order.
#pragma JessieIntegerModel(math)

/*@ predicate Sorted{L}(int *a, integer l, integer h) =
  @   \forall integer i,j; l <= i <= j < h ==> a[i] <= a[j] ;
  @*/

/*@ requires \valid_range(t,0,n-1);
  @ ensures Sorted(t,0,n-1);
  @*/
void insert_sort(int t[], int n) {
  int i,j;
  int mv;
  if (n <= 1) return;
  /*@ loop invariant 0 <= i <= n;
    @ loop invariant Sorted(t,0,i);
    @ loop variant n-i;
    @*/
  for (i=1; i<n; i++) {
    // assuming t[0..i-1] is sorted, insert t[i] at the right place
    mv = t[i]; 
    /*@ loop invariant 0 <= j <= i;
      @ loop invariant j == i ==> Sorted(t,0,i);
      @ loop invariant j < i ==> Sorted(t,0,i+1);
      @ loop invariant \forall integer k; j <= k < i ==> t[k] > mv;
      @ loop variant j;
      @*/
    // look for the right index j to put t[i]
    for (j=i; j > 0; j--) {
      if (t[j-1] <= mv) break;
      t[j] = t[j-1];
    }
    t[j] = mv;
  }
}


/*
Local Variables:
compile-command: "frama-c -jessie insertion_sort.c"
End:
*/

The proof is automatic with any SMT solver.