Insertion sort as in Sedgewick

module InsertionSort

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.IntArraySorted
  use import array.ArrayPermut
  use import array.ArrayEq

  let insertion_sort (a: array int) =
    ensures { permut_all (old a) a }
'L:
    for i = 1 to length a - 1 do
      invariant { permut_all (at a 'L) a }
'L1:
      let v = a[i] in
      let j = ref i in
      while !j > 0 && a[!j - 1] > v do
        invariant { 0 <= !j <= i }
        invariant { permut_all (at a 'L1) a[!j <- v] }
'L2:
        a[!j] <- a[!j - 1];
        assert { exchange (at a 'L2)[!j <- v] a[!j-1 <- v] (!j - 1) !j};
        j := !j - 1
      done;
      a[!j] <- v
    done

end