Examples
lA searching program:
lInput assertion: a == a0
lOutput assertion: Index m is such that
la == a0, and
la[m] == v if v occurs in array a, and
lm == -1   if v does not occur in array a