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?