val N:ℕ;
val M:ℕ;
axiom notZero ⇔ N > 0 ∧ M > 0;

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

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