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).