source: CIVL/examples/verifyThis/pairInsertSort.cvl

typedef int T;
$input int n, N = 5, LEFT, RIGHT;
$assume(1<=n && n<=N && 1<=LEFT && LEFT<=RIGHT && RIGHT<n);
$input T A[n];
int count(int n, T *p, int val) {
  int result = 0;
  for (int i=0; i < n; i++) if ((p[i]) == val) result++;
  return result;
}
/* Asserts the sequence starting at p2 is the permutation of that
 * starting at p1 with elements occurring in nondecreasing order */
void assertSortOf(int n, T *p1, T *p2) {
  $assert($forall (int i : 0..n-2) p2[i]<=p2[i+1]);
  $assert($forall (int i : 0..n-1) $exists (int j : 0..n-1) p1[i]==p2[j]);
  for (int i=0; i<n; i++) $assert(count(n, p1, p2[i]) == count(n, p2, p2[i])); 
}
int main() {
  for (int i=LEFT; i<=RIGHT; i++) $assume(A[LEFT-1]<=A[i]);
  int a[n];
  for (int i=0; i<n; i++) a[i]=A[i];
  int left = LEFT, right = RIGHT;
  for (int k = left; ++left <= right; k = ++left) {
    int a1 = a[k], a2 = a[left];
    if (a1 < a2) { a2 = a1; a1 = a[left]; }
    while (a1 < a[--k]) a[k + 2] = a[k];
    a[++k + 1] = a1;
    while (a2 < a[--k]) a[k + 1] = a[k];
    a[k + 1] = a2;
  }
  int last = a[right];
  while (last < a[--right]) a[right + 1] = a[right];
  a[right + 1] = last;
  $assert($forall (int i:0..LEFT-1) a[i]==A[i]);
  $assert($forall (int i:RIGHT+1..n-1) a[i]==A[i]);
  assertSortOf(RIGHT-LEFT+1, A+LEFT, a+LEFT);
}