val N:ℕ;
val M:ℕ;
// ≤ ≥ ≠ ∨ ∧ ¬ ∃ ∀ ∈ ⇔ ⇒ ⇐
type index = ℤ[-N,N];
type elem  = ℤ[-M,M];
type array = Array[N,elem];

// preconditions
pred preMax_lengthGTOne(n:index) ⇔ n ≥ 1;

// postconditions
pred postMax_IndexMustBeValid(p:index, n:index) ⇔ 0 ≤ p ∧ p < n;
pred postMax_ElemHasToBeMax(a:array, p:index, n:index) ⇔
	∀k:index . 0 ≤ k ∧ k < n ⇒ a[p] ≥ a[k];
pred postMax_condition(a:array, p:index, n:index) ⇔
	postMax_IndexMustBeValid(p, n) ∧ postMax_ElemHasToBeMax(a, p, n);

proc maximum(a:array, n:index): index
	requires preMax_lengthGTOne(n);
	ensures postMax_condition(a, result, n);
{
  var p:index ≔ n-1;
  var m:elem ≔ a[p];
  var i:index ≔ p-1;
  while i ≥ 0 do
   	invariant i < n;
   	invariant 0 ≤ p ∧ p < n;
   	invariant m = a[p];
   	invariant ∀k:index . i < k ∧ k < n ⇒ a[k] ≤ m;
   	decreases i+1;
  {
    if a[i] > m then
    {
      p ≔ i;
      m ≔ a[p];
    }
    i ≔ i-1;
  }
  return p;
}
// ≤ ≥ ≠ ∨ ∧ ¬ ∃ ∀ ∈ ⇔ ⇒ ⇐

// preconditions
pred preSort_nGEQZero(n:index) ⇔ n ≥ 0;
// postconditions
pred postSort_isSorted(a:array, n:index) ⇔
	∀k:index . 0 ≤ k ∧ k < n-1 ⇒ a[k] ≤ a[k+1];

proc sort(a:array, n:index): array
	requires preSort_nGEQZero(n);
	ensures postSort_isSorted(result, n);
{
  var b:array ≔ a;
  var i:index ≔ n;
  while i > 1 do
  	invariant i > 1 ⇒ i = n;
  	//invariant ∀k:index . 0 ≤ k ∧ k < n-1 ⇒ a[k+1] ≥ b[k];
  	invariant 0 < i ∧ i < n ⇒ ∀k:index . i ≤ k ∧ k < n-1 ⇒ b[k] ≤ b[k+1];
  	decreases if i > 1 then i-1 else 0;
  {
    var j:index ≔ maximum(b, i);
    i ≔ i-1;
    if i ≠ j then
    {
      var e:elem ≔ b[i];
      b[i] ≔ b[j];
      b[j] ≔ e;
    }
  }
  return b;
}