Proving the Assertions (8)
We use the established the loop invariant: (("k < i) a[k] != v ô i < a.length)
((   k) a[k] != v)
Text Box: A
The program can get to the second exit only if  i > a.length.
Substituting in the invariant:
((   k < a.length) a[k] != v)
Text Box: A
But this is the same as
The program has now been established to be partially correct.

To show total correctness, we must establish termination as well.
Termination is ÒobviousÓ because the number of steps in the loop
is bounded by the length of the array.