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 { sorted a }
    for i = 1 to length a - 1 do
      invariant { sorted_sub a 0 i }
      let v = a[i] in
      let j = ref i in
      while !j > 0 && a[!j - 1] > v do
        invariant { 0 <= !j <= i }
        invariant { forall k1 k2: int. 0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2] }
        invariant { forall k: int. !j+1 <= k <= i -> v < a[k] }
        a[!j] <- a[!j - 1];
        j := !j - 1
      done;
      a[!j] <- v
    done

end