lInput assertion: n > 0 and a == a0
lOutput assertion: Index m is index of a maximal value in a and a == a0
lWithout the anchor, the assertion could be satisfied without the program
actually computing the maximum; it could simply set all
elements of a to 0 and m to 0, and the assertion would be
satisfied; a == a0 prevents the array from being modified
overall.