Proving the Assertions (2)
We want establish that the loop
invariant is true
every time the program gets to the
point shown
(right before the test i < a.length).
Use transition
induction:
Basis: The assertion is true the first time the
program gets to that point.
Induction Step: Assume it is true for an
arbitrary time; show it is true the next
time (if there is a next time).