val N:ℕ;
val M:ℕ;
axiom notNull ⇔ N ≥ 1;

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

proc maximum(a:array,n:int):int
  requires 1 ≤ n ∧ n ≤ N;
  ensures 0 ≤ result ∧ result < n;
  ensures ∀k:int. 0 ≤ k ∧ k < n ⇒ a[result] ≥ a[k]; 
{
  var p:int  ≔ n-1;
  var m:elem ≔ a[p];
  var i:int  ≔ p-1;
  while i ≥ 0 do
  {
    if a[i] > m then { p ≔ i; m ≔ a[p]; }
    i ≔ i-1;
  }
  return p;
}

proc sort(a:array): array
{
  var b:array ≔ a;
  var i:int   ≔ N;
  while i > 1 do
  {
    var j:int ≔ maximum(b,i);
    i ≔ i-1;
    if i ≠ j then { var e:elem ≔ b[i]; b[i] ≔ b[j]; b[j] ≔ e; }
  }
  return b;
}