Proving the
Assertions (8)
We use the
established the loop invariant: (("k < i) a[k] != v ô i <
a.length)
(( k)
a[k] != v)
The program can get to
the second exit only if i > a.length.
Substituting in the
invariant:
(( k <
a.length) a[k] != v)
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.