val N:ℕ;
val M:ℕ; axiom MnotZero ⇔ M > 0;

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

proc maximumElement(a:array,n:index): elem
{
  var m:elem; 
  var i:index;
  m ≔ -1; 
  i ≔ 0;
  while i < n do
  {
    if a[i] > m then m ≔ a[i];
    i ≔ i+1;
  }
  return m;
}