The Need for ÒAnchorsÓ
lInput assertion: n > 0 and a == a0 
lOutput assertion: Index m is index of a maximal value in a and a == a0
l
l
l
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.
Why is this necessary?