Loop invariants (Specifically Ch.3 of "Accelerated C++")

Question

I'm currently working my way through "Accelerated C++" and just came across this in chapter 3:

// invariant:
//  we have read count grades so far, and
//  sum is the sum of the first count grades
while (cin >> x) {
    ++count;
   sum  +=  x;
}

The authors follow this by explaining that the invariant needs special attention paid to it because when the input is read into x, we will have read count + 1 grades and thus the invariant will be untrue. Similarly, when we have incremented the counter, sum will no longer be the sum of the last count grades (in case you hadn't guessed, it's the traditional program for calculating student marks).

What I don't understand is why this matters. Surely for just about any other loop, a similar statement would be true? For example, here is the book's first while loop (the output is filled in later):

// invariant: we have written r rows so far
while (r != rows) {
    // write a row of output 
    std::cout << std::endl;
    ++r;
}

Once we have written the appropriate row of output, surely the invariant is false until we have incremented r, just as in the other example?

What makes these two conditions different?

EDIT: Thanks for all your replies. I think I've got it but I'm going to leave it going a little longer before I choose an "Accepted answer" just to be sure. So far, all the replies basically agree so it hardly seems fair, but worth doing I guess.

The original paragraph, as requested below:

"Understanding the invariant for this loop requires special care, because the condition in the while has side effects. Those side effects affect the truth of the invariant: Successfully executing cin >> x makes the first part of the invariant-the part that says that we have read count grades-false. Accordingly, we must change our analysis to account for the effect that the condition itself might have on the invariant.

We know that the invariant was true before evaluating the condition, so we know that we have already read count grades. If cin >> x succeeds, then we have now read count + 1 grades. We can make this part of the invariant true again by incrementing count. However, doing so falsifies the second part of the invariant-the part that says that sum is the sum of the first count grades-because after we have incremented count, sum is now the sum of the first count - 1 grades, not the first count grades. Fortunately, we can make the second part of the invariant true by executing sum += x; so that the entire invariant will be true on subsequent trips through the while.

If the condition is false, it means that our attempt at input failed, so we didn't get any more data, and so the invariant is still true. As a result, we do not have to account for the condition's side effects after the while finishes."

Answer 1

In general, invariants are understood to only apply between iterations of the loop. (At least that's how I read them!)

The general case looks like:

[invariant true];
while (keep going) {
    [state transformation];
    [invariant true];
}

But during the state transformation, your invariant does not necessarily hold true.

And as a separate style note: if you want to be a super coder, instead of leaving your invariants in comments, make them assertions!

// Loop invariant: x+y = -4
for (int x = 0; x < 10; x++) {
    [do something];
    assert(x+y == -4);  // Loop invariant here!
}

That way you have self-checking code.

Answer 2

From your description it sounds like the author is talking nonsense. Yes, the invariant becomes untrue temporarily between instructions, but that is going to happen whenever you have non-atomic operations like this. As long as there aren't any clear break points that could lead to the invariant being incorrect and the program in an inconsistent state, you are fine.

In this case, the only way that could happen is if std::cout throws an exception while an invariant is untrue, then you catch that exception somewhere but continue execution in a bad state. It seems to me the author is being overly pedantic. So again, as long as you don't have any break/continue statements in the wrong place or exceptions being thrown you are OK. I doubt many people would bother focusing on your example code because it's just so simple.