val N:ℕ;
val M:ℕ;

// type index must contain -1
val N0:ℤ[-N-1,-1] = if N=0 then -1 else -N;
val N1:ℤ[1,N+1]   = -N0;

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

proc maximumIndex(a:array): index
{
  var p:index;
  if N = 0 then
    p ≔ -1;
  else
  {
    p ≔ 0;
    var m:elem ≔ a[0];
    var i:index ≔ 1;
    while i < N do
    {
      if a[i] > m then
      {
        p ≔ i;
        m ≔ a[p];
      }
      i ≔ i+1;
    }
  }
  return p;
}