CS 477/677 Loop Invariant Problems

A loop invariant is a condition associated with a loop that has the following properties.
  1. It is true before the first iteration of the loop starts.
  2. If it is true at the beginning of one iteration of the loop, it is true at the end of that iteration of the loop.
It follows by induction that, if the loop terminates normally, the loop invariant will be true after the loop terminates.
Do not confuse the loop invariant with the loop condition.
Piece of advice: to more easily see the loop invariant, it is best to convert a for loop to a while loop.
  1. Find the loop invariant of the loop in this code.
  2. This code has two loops. Find the loop invariant of each of them.
  3. Find the loop invariant of the loop in this code.