Proving the
Assertions (4)
Induction Step: Assume
it is true for an
arbitrary time; show it is true the next
time (if there is a next time).
Assume the assertion is
true now.
Suppose there is a next
time the program gets
to that point.
What
happened in between?
(("k <
i) a[k] != v ô i <
a.length)