val N:ℕ; val M:ℕ; type index = ℤ[-N,N]; type elem = ℤ[-M,M]; type array = Array[N,elem]; proc maximumIndex(a:array,n:index): 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; }