Specification Example
lA program that finds the index of a maximal value in an array a of n > 0 elements.

lAn array max-finding program:
lInput assertion: n > 0.
lOutput assertion:
("i) (i > 0 ô i < n) ¨ a[i] < a[m]

(ÒIndex m is index of a maximal value in a.Ó)

lIs this adequate as a specification?