Loop invariants is the topic of the problem in this note.

while_a.pdf