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
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.