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

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.

Answer 2

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 3

I believe the book is referring to the way that the while loops are stopped. In the second case it is very easy to see that the loop will stop once "r" has been incremented enough to equal "rows". Because most counts in C++ are zero based this will most likely output a line for each row.

On the other hand, the first example is using the operator overload for ">>" on the cin object. The while loop will continue as long as this function does not return a zero. That operator overload will not return this value until the input has closed.

What key can you press to make "cin >>" return a 0? Otherwise the loop will never end. You need to make sure you don't create a loop like that.

Adding a line to stop the loop outside of the condition is needed. Look up the "break" and "continue" statements.

Answer 4

This is really interesting/important in the context of exception safety.

Consider the following scenario:

• "count" is a user-defined class with an overloaded operator++
• That overloaded operator++ throws an exception.
• The exception is caught later outside the loop (i.e. the loop looks like it does now, there's no try/catch)

In that case, the loop invariant no longer holds, and the state of everything going on in the loop is in question. Was the row written? Was the count updated? Is the sum still correct?

Some extra protection (in the form of temporary variables to hold intermediate values and some try/catches) needs to be used to ensure that everything remains consistent even when an exception is thrown.

Answer 5

The book seems to complicate things a lot more than it should. I really don't think explaining loops with invariants is a good thing. It's kind of like explaining addition with quantum physics.

The authors follow this by explaining that the invariant needs special attention paid to it because when the input is read into the variable x, we will have read count+1 grades and thus the invariant will be untrue. Similarly, when we have incremented the counter, the variable 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).

First of all the invariant isn't clear. If the invariant is "at the end of an iteration of the while loop, we have read count grades with the sum of sum", then that looks correct to me. The invariant isn't clearly specified, so it makes no sense to even talk about when it is and isn't respected.

If the invariant is "at any point of an iteration of the while loop, we have read ...`, then, strictly speaking, that invariant will not be true. As far as loops are concerned, I think an invariant should refer to the state that exists at the beginning, end, or a fixed point in the loop.

I don't have that book and I don't know if things get clarified or not, but it seems to be using invariants wrong. If their invariant isn't true, why even bother using one in the first place?

I don't think you should worry about this too much. As long as you understand how these loops work, you're fine. If you want to understand them through invariants, you can, but you must pay attention to the invariant you choose. Don't pick a bad one, or it defeats the purpose. You should pick an invariant for which it is easy to write code that respects it, not pick a random one and then struggle to write code that respects it, and definitely do not pick a vague one and write code that has nothing to do with it and then say "one must pay attention as this doesn't actually respect the vague invariant I chose".

What I don't understand is why this matters. Surely for just about any other loop, a similar statement would be true?

It depends on the invariant used (the book is pretty vague about that from what you said), but yes, you seem to be correct in this case.

For this code:

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

The invariant "At the end of an iteration of the while loop, we have written r rows" is definitely true.

I don't have the book, so I don't know if these things are all addressed later on. From what you said though, this seems like a really lousy way to explain loops.

Answer 6

I agree that you have to know what the invariant is. Say I am writing good old BankAccount. I may say that always and at all times, the total of all the transactions in the transaction history will add up to the balance of the account. That sounds sensible. It would be good for it to be true. But during the handful of lines when I am processing a transaction, it isn't true. Either I update the balance first, or I add the transaction to the history and update the balance. For a moment the invariant isn't true.

I can imagine a book that wants you to understand that an invariant is something you claim to be true always and at all times, but that sometimes isn't, and that it is good to know when it isn't true, because if you return, or throw an exception, or yield to concurrency, or whatever, when it isn't true, then your system will be all messed up. It's a little harder to imagine that your paraphrase is what the authors intended to say. But I guess if I turn my head sideways and squint I can rephrase it as "sum is the sum of the first count grades" is true always and at all times except right while we're busy reading and adding them - it might not be true during that process. Make sense?

Answer 7

Following your update, the author correctly describes how a loop invariant has to be “recovered” in every iteration of a loop.

What I don't understand is why this matters. Surely for just about any other loop, a similar statement would be true?

Yes, that’s true – there’s nothing special about this loop (OK, the loop condition has a side-effect but this can easily be rewritten).

But I think the important fact that the author wanted to point out is this: after an action performed inside the loop the loop invariant isn’t generally true any more. This of course is a problem for the invariant unless subsequent statements correct this by taking appropriate actions.

Answer 8

On the first example the count variable is not being used for anything else than just be incremented for each input loop. The loop will continue until >> returns NULL.

On the second example, rows must be initialized with the number of rows to be written. The loop will continue until the number of rows specified be written.

while (cin >> x) {
    ++count;
}


rows = NROWS;
r = 0;

while (r != rows) {
    // write a row of output 
    std::cout << std::endl;
    ++r;
}