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.