Proving loop invariant for a possibly nonterminating while loop

Question

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.

1. $S(0)$ base case holds because adding 0 can't change the value and sum already starts with 0.
2. 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.

Answer 1

There's no need to perform an explicit induction here. Notice how your proposed invariant doesn't refer to the number of loop iterations. You're on the right track. Let $I \equiv \text{sum}\geq 0$ be our candidate loop invariant.

To show that $I$ is indeed a loop invariant it suffices to show that

• $I$ holds when control reaches the loop for the first time and
• $I$ is re-established by the loop body, assuming $I$ held before and the loop test (here $x\geq 0$) was true as well.

This already guarantees that $I$ will also hold upon loop termination. (Actually, even $I\land \neg(x\geq 0)$ since the loop test cannot be true anymore, but you don't need that in this example.)

The assignment statement $\text{sum} = 0$ establishes $I$ because $0\geq 0$. To do that more formally we'd use Hoare logic.

Working backwards from $I$ through the loop body we notice that the reading into $x$ doesn't affect $\text{sum}$, so we still have $I$. Pushing further backwards through the assignment statement, we arrive at $K\equiv \text{sum}+x\geq 0$ (by substituting the right-hand-side of the assignment for the occurrences of the left-hand-side in $I$). We need to prove that $I\land x\geq 0$ implies $K$, but that's trivial.