CSE 131 Module 3: Iteration

Loop Invariants

You were given the following code as partof Quiz 3:
```int ans = 0;
int i   = a;

while (__________________________ ) {  // fill in the loop predicate
i   =   i - b
ans = ans + 1
}
// ans is now a/b
```
The code is supposed to compute ans as the int result of dividing a by b.
1. Develop a loop invariant for the above code that can be used to prove that ans = a/b using integer division.
You should show your loop invariant to the instructor before proceeding, to be sure that you have a proper loop invariant
2. Write a mathematical proof of the loop's correctness. Every step must proceed from what came before it, with no gaps in logic. Any flaw will cause your submission to be rejected, but you can continue revising your proof until the end of the semester when extensions are finally due.
3. When the loop is over, what is the strongest statement you can make about i?
Check this with the instructor too.
4. Prove that your statement about i is correct.
Submit the above to the instructor with your name and the last 3 digits of your student ID.

You will be asked to explain steps of your proof, so you better understand what you write if you want to get credit for it.