// -------------------------------------------------------------------
// Sorting arrays by the "insertion sort" algorithm
// -------------------------------------------------------------------

val N:ℕ;
val M:ℕ;

type elem = ℕ[M];
type array = Array[N,elem];
type index = ℤ[-1,N]; // also includes -1 and N

proc sort(a:array): array
  ensures ∀k1:index,k2:index. 
    0 ≤ k1 ∧ k1 < k2 ∧ k2 < N ⇒ result[k1] ≤ result[k2];
  ensures ∃p:Array[N,index]. 
    (∀k:index. 0 ≤ k ∧ k < N ⇒ 0 ≤ p[k] ∧ p[k] < N) ∧
    (∀k1:index,k2:index. 
      0 ≤ k1 ∧ k1 < N ∧ 0 ≤ k2 ∧ k2 < N ∧ k1 ≠ k2 ⇒ p[k1] ≠ p[k2]) ∧
    (∀k:index. 0 ≤ k ∧ k < N ⇒ a[k] = result[p[k]]);
{
  var b:array = a;
  for var i:index ≔ 1; i < N; i ≔ i+1 do
  {
    var x:elem ≔ b[i];
    var j:index ≔ i-1;
    while j ≥ 0 ∧ b[j] > x do
    {
      b[j+1] ≔ b[j];
      j ≔ j-1;
    }
    b[j+1] ≔ x;
  }
  return b;
}

