# Proving loop invariant for a possibly nonterminating while loop

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.

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.

• I understand this and much appreciated but, theme of the chapter being proving loop invariants by induction, I was expecting there would be an inductive proof too. In a sense, this is for the case of being exercise-complete, while reading the book. Would be nice if you can also share an inductive proof (or showing that an inductive proof is not possible). Feb 3 at 9:01
• The essence of the proof technique goes back to Floyd, who devised it for flow charts/transition diagrams. The soundness proof of his (any every later) assertional reasoning method involves one proof by induction, typically on the number of steps in the execution of a program. When applying such a method, there's no more need for an induction.
– Kai
Feb 3 at 22:53