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.Ó)
("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?