// ----------------------------------------------------------------------------
// Sorting arrays by the Insertion Sort Algorithm
// ----------------------------------------------------------------------------

val N:ℕ;
val M:ℕ;

type elem = ℕ[M];
type array = Array[N,elem];
type index = ℕ[N-1];

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