Examples
l
A
searching
program:
l
Input assertion: a == a
0
l
Output assertion: Index m is such that
l
a == a
0
, and
l
a[m] == v if v occurs in array a, and
l
m == -1
if v does not occur in array a
l