I started studying through Aho, Ullman - Foundations of Computer Science as a free time exercise. In the second chapter about loop invariants and inductive proofs, there is a starred exercise.
int sum = 0;
scanf("%d", &x);
while(x >= 0) {
sum = sum + x;
scanf("%d", &x);
}
printf("%d", sum);
Read a number into x
, accumulate it into sum
variable if x
is nonnegative, and move on with the loop until user enters a negative number. Pretty simple stuff. Intuitively, we can readily see the printf
output will be a nonnegative number. This is the thing we want to prove.
My loop invariant choice is:
Before every check of loop condition, value of
sum
is nonnegative.
Of course, in line with the aim of the chapter, we also need to prove this invariant by induction. I can't come up with a rigorous formulation for an inductive proof myself.
Here is a bogus attempt:
$$S(x): If \hspace{0.4em} x\geq0, sum \geq 0$$
Proof is by induction on the value of variable x
.
- $S(0)$ base case holds because adding 0 can't change the value and sum already starts with 0.
- Assume $S(n)$ is true. How to use the inductive hypothesis?
I can't formulate this. I am more used to utilizing the number of iteration of the loop (i) to base my inductive proof on and say "such and such is true before the $i^{th}$ iteration. But in this example, there is no easy way to talk about the number of iteration in terms of program variables sum
and x
.