Proving the Assertions (6)
So far we have
established the loop invariant: (("k < i) a[k] != v ô i <
a.length)
Now concentrate on establishing the
output assertion:
There are two places the program can exit:
In the first place, it is obvious that a[r] == v,
since we just tested a[i] == v and
set r = i.
In the second place, we claim that
(("k <
a.length) a[k] != v ^ r == -1
This conjunct
is obvious.
How do we show
the first conjunct?
