Loop invariants

Why this matters

Suppose a loop prints a number and you want to know whether the number is right. You can run the program on a few inputs and compare the output with what you expected. Testing is useful, but a test only tells you about the inputs you tried. A loop can be right for ten inputs and wrong for the eleventh.

A loop invariant is a different kind of check. It is a statement about your variables that you can reason about for every input. When you can state the invariant, you can explain why the loop gives the right answer, and you can point to the exact place where it would stop being right. Engineers use this when they read someone else's loop, when a loop gives a wrong answer on one rare input, and when they write a new loop and want to be sure of it before running it.

This lesson uses sums and maximums because the statements are short. The loop patterns themselves are covered in the lessons on for loops and sentinel loops, so only the parts needed for the proofs appear here.

The idea: a fact that stays true

A loop invariant is a statement about your variables that is true every time the loop is about to run its test. The word "invariant" means "does not change". The variables do change on every pass. The statement about them does not stop being true.

Here is an everyday example. You have a jar of coins and a pile of paper. You take one coin out of the jar at a time, put it on the pile, and write down a count. Your statement is: "the count equals the number of coins on the pile." Before you take the first coin, the pile is empty and the count is 0, so the statement is true. Each time you move one coin, you add one to the count, so the statement is still true. When you stop, the statement tells you the count is the number of coins on the pile. You did not need to recount the pile to know that.

Every loop invariant has three parts, and you check each one:

1. Start. Before the first pass, the statement must be true. This is the check on the starting values.
2. Keep. If the statement is true before a pass, it must still be true after that pass. This is the check on the body of the loop.
3. End. When the loop stops, the statement is still true, and the test is the reason the loop stopped. Put those two facts together and you often have the answer.

The second part is the one that does most of the work. You do not have to prove the loop from the first pass to the last. You only have to show that one pass keeps the statement true. The rest follows from repeating it.

Example 1: the sum of 1 to 5

Here is a loop that adds the numbers from 1 to 5 and prints the total after each pass.

#include <iostream>
 
int main() {
    int total = 0;
    for (int k = 1; k <= 5; ++k) {
        total += k;
        std::cout << "after pass " << k << ": total = " << total << '\n';
    }
    std::cout << "final total = " << total << '\n';
}

Compile and run it with g++ -std=c++20 -Wall. The output is:

after pass 1: total = 1
after pass 2: total = 3
after pass 3: total = 6
after pass 4: total = 10
after pass 5: total = 15
final total = 15

The invariant for this loop is: after each pass, total is the sum of the numbers from 1 up to k. The table shows the same fact pass by pass.

Now check the three parts.

Start. Before the first pass there are no numbers added yet, so total should be the sum of an empty list, which is 0. The code sets total to 0. The statement is true.

Keep. Suppose that before a pass with counter k, total is the sum from 1 to k - 1. The pass adds k, so total becomes the sum from 1 to k. The statement is true after the pass.

End. The loop stops when k is 6, because the test k <= 5 is false. Before that point, total was kept equal to the sum from 1 to k, so at the end it is the sum from 1 to 5, which is 15.

You did not have to trust the table. The proof covers every pass, including passes you did not print.

Writing the invariant as a check

A comment that says the invariant is useful, but a comment cannot fail. C++ has a tool that can. assert is a line that checks a condition and stops the program with a message if the condition is false. You put an assert in the loop to check the invariant on every pass.

#include <cassert>
#include <iostream>
 
int main() {
    const int n = 5;
    int total = 0;
    for (int k = 1; k <= n; ++k) {
        total += k;
        // invariant: total is the sum of 1..k
        assert(total == k * (k + 1) / 2);
    }
    std::cout << "sum of 1.." << n << " = " << total << '\n';
}

Output:

sum of 1..5 = 15

The check k * (k + 1) / 2 is the formula for the sum of 1 to k, so the assert says the loop's total matches the formula on every pass. The program did not stop, so the invariant held for all five passes. When a program is built with NDEBUG defined, the compiler removes every assert. Use asserts while you learn and while you test. Do not depend on them for checks that must always run in the finished program.

Example 2: the largest value

Now a loop with a harder invariant. You want the largest number in a list.

Pick a variable called best to hold the answer so far. The invariant has two parts:

• best is one of the values you have looked at so far.
• best is at least as large as every value you have looked at so far.

The first part is what makes a starting value legal. Here is the loop.

#include <cstddef>
#include <iostream>
#include <vector>
 
int main() {
    std::vector<int> values{4, -7, 12, 3, 12, 9};
    if (values.empty()) {
        std::cout << "no values\n";
        return 0;
    }
    int best = values[0];
    for (std::size_t i = 1; i < values.size(); ++i) {
        if (values[i] > best) {
            best = values[i];
        }
    }
    std::cout << "max = " << best << '\n';
}

Output:

max = 12

Start. The loop starts with best = values[0]. After looking at one value, best is that value. It is one of the values seen, and it is at least as large as all of them. Both parts are true.

Keep. Suppose that before a pass, best is the largest value seen so far, and the pass looks at a new value v. If v is bigger than best, the code sets best to v. Now best is v, which is bigger than everything seen before, so it is the largest of the values seen now. If v is not bigger, best stays the same. It is still the largest of the old values, and v is not bigger than it, so it is still the largest of the new set. Both parts of the invariant hold after the pass.

End. The loop stops when i equals the number of values. Every value has been looked at, so best is the largest value in the list.

Why the starting value matters

Many beginners start best at 0. That looks harmless, and it is wrong for any list where every value is negative. Look at what the invariant says in that case. Before the first pass, the first part of the invariant claims that best is one of the values seen. No values have been seen yet, and 0 is not in the list, so the claim is false from the start. Here is the loop with the bad start.

#include <cstddef>
#include <iostream>
#include <vector>
 
int main() {
    std::vector<int> values{-4, -7, -12, -3};
    int best = 0;  // wrong start: 0 is not in the list
    for (std::size_t i = 0; i < values.size(); ++i) {
        if (values[i] > best) {
            best = values[i];
        }
    }
    std::cout << "max = " << best << '\n';
}

Output:

max = 0

The program does not crash and does not warn. It prints 0, which is not in the list. The invariant tells you where to look: the start is false, so every pass after it starts from a false statement.

Checking the invariant on every pass

You can put the two-part invariant in an assert and check it after every pass. The inner loop below is slow, because it looks back over the whole list on each pass. It is for learning, so you can see the invariant hold.

#include <cassert>
#include <cstddef>
#include <iostream>
#include <vector>
 
int main() {
    std::vector<int> values{4, -7, 12, 3, 12, 9};
    int best = values[0];
    for (std::size_t i = 1; i < values.size(); ++i) {
        if (values[i] > best) {
            best = values[i];
        }
        // invariant: best is at least every value in values[0..i]
        // and best is equal to one of them
        bool equals_one = false;
        for (std::size_t j = 0; j <= i; ++j) {
            assert(best >= values[j]);
            equals_one = equals_one || best == values[j];
        }
        assert(equals_one);
        std::cout << "pass " << i << ": best = " << best << '\n';
    }
    std::cout << "max = " << best << '\n';
}

Output:

pass 1: best = 4
pass 2: best = 12
pass 3: best = 12
pass 4: best = 12
pass 5: best = 12
max = 12

Each line of output is printed only after both asserts passed for that pass.

Example 3: the index of the largest value

Sometimes you need the position of the largest value, not the value itself. The same idea works. Keep the index in a variable and let the invariant say what it points to.

Invariant: values[best_index] is the largest of the values from index 0 up to i - 1.

#include <cstddef>
#include <iostream>
#include <vector>
 
int main() {
    std::vector<int> values{4, -7, 12, 3, 12, 9};
    std::size_t best_index = 0;
    for (std::size_t i = 1; i < values.size(); ++i) {
        // invariant: values[best_index] is the largest of values[0..i-1]
        if (values[i] > values[best_index]) {
            best_index = i;
        }
    }
    std::cout << "max " << values[best_index] << " at index " << best_index << '\n';
}

Output:

max 12 at index 2

The value 12 appears twice, at index 2 and index 4. The output names index 2. The invariant explains why: the test is >, not >=. When a later value is equal to the current best, the test is false and the index stays at the earlier position. If you change the test to >=, the output becomes index 4, and the invariant still holds. Both answers are correct for "the largest value", but the invariant tells you which one your code produces.

Example 4: a sum with a condition

Adding a condition does not change the method. Here the invariant is about the sum of the even numbers.

#include <cassert>
#include <cstddef>
#include <iostream>
#include <vector>
 
// Sum of the even values in a list, with the invariant checked on every pass.
int sum_of_evens(const std::vector<int>& values) {
    int total = 0;
    for (std::size_t i = 0; i < values.size(); ++i) {
        if (values[i] % 2 == 0) {
            total += values[i];
        }
        // invariant: total is the sum of the even values in values[0..i]
        int expected = 0;
        for (std::size_t j = 0; j <= i; ++j) {
            if (values[j] % 2 == 0) {
                expected += values[j];
            }
        }
        assert(total == expected);
    }
    return total;
}
 
int main() {
    std::vector<int> values{3, 8, -4, 7, 10, 1};
    std::cout << "sum of evens = " << sum_of_evens(values) << '\n';
}

Output:

sum of evens = 14

The even values are 8, -4 and 10. Their sum is 14. Note that -4 % 2 is 0 in C++, so negative even numbers are handled by the same test.

The invariant says total matches the sum of the even values seen so far. The condition values[i] % 2 == 0 decides whether the current value is added. Both branches keep the invariant true, which is the proof for this loop.

Example 5: the average, built from a sum

An average is a sum divided by a count, so it needs two loop invariants that work together. Build the loop from the invariants first, then write the code that keeps them true.

The two invariants are:

• total is the sum of values[0] up to values[i - 1].
• The count of values looked at is i. This count is not a separate variable here, because the index already holds it.

Before the first pass, i is 0 and total is 0. The sum of an empty list is 0, so the first invariant is true. Each pass adds values[i] to total and moves i forward by one, so the first invariant is true again after the pass.

When the loop ends, i equals the size of the list, so total is the sum of every value. Dividing by the size gives the average.

#include <cstddef>
#include <iostream>
#include <vector>
 
int main() {
    std::vector<int> values{4, -7, 12, 3};
    int total = 0;
    for (std::size_t i = 0; i < values.size(); ++i) {
        // invariant: total is the sum of values[0..i-1]
        total += values[i];
    }
    // after the loop, total is the sum of all values
    double average = static_cast<double>(total) / static_cast<double>(values.size());
    std::cout << "sum = " << total << ", count = " << values.size()
              << ", average = " << average << '\n';
}

Output:

sum = 12, count = 4, average = 3

The division uses double, not int. Integer division would drop the fraction, so an average of 3.5 would print as 3. The cast to double happens on both numbers before the division, so the result has a fraction part. The loop itself does not change. Only the last line of the program uses the two counts.

The empty list is the same case as before. The average of zero values divides 0 by 0, which gives nan (not a number) for doubles, so the program must check the size before it divides.

Using the invariant to find a bug

The invariant tells you what the loop has done after each pass. The end of the loop tells you whether that is what you wanted. The mismatch between those two is the bug.

Here is a loop that is meant to add 1 to 5, with a mistake in the test.

#include <cassert>
#include <iostream>
 
int main() {
    const int n = 5;
    int total = 0;
    for (int k = 1; k < n; ++k) {  // bug: should be k <= n
        total += k;
        assert(total == k * (k + 1) / 2);  // holds on every pass that runs
    }
    assert(total == n * (n + 1) / 2);  // checked after the loop: fails
    std::cout << "total = " << total << '\n';
}

Run it and the program stops:

assert_fail: assert_fail.cpp:11: int main(): Assertion `total == n * (n + 1) / 2' failed.

The first assert in the loop never fails. The loop runs for k equal to 1, 2, 3 and 4, and for each of those passes total is the sum from 1 to k. The bug is that the loop stops before it reaches 5. The loop's invariant is true, but its promise, that total ends up as the sum from 1 to 5, is false. The check after the loop catches exactly that gap. Use this habit: state what the loop promises at the end, and check it.

Without the check after the loop, the program prints total = 10 and gives no sign that anything is wrong. The invariant on each pass was true, so it would be easy to miss.

Proving the loop ends

The invariant says what is true when the loop stops, but it does not say that the loop stops. You need a second fact: the counter moves toward the end of its range on every pass. In the examples above, i or k goes up by one each time, and the loop ends after a fixed number of passes. The lesson on step and reverse ranges covers counters that move in other ways, including the cases where the loop never ends.

Common mistakes

A starting value that is not in the data

This is the mistake shown in Example 2. Setting best = 0 for a list of negative numbers gives a result that is not in the list. The program runs without any message. The check is to ask, before writing the loop, what best must be before the first pass. For a maximum, the first value of the list is always a legal start, and the empty list needs its own check.

An off-by-one at the end

The bug in the assert example above, k < n instead of k <= n, is the usual form. The output for a bad version looks reasonable, which is why the check after the loop matters. A typical failed assert looks like this:

assert_fail: assert_fail.cpp:11: int main(): Assertion `total == n * (n + 1) / 2' failed.

The message names the file and the line, and it shows the exact condition that was false. Read the condition first. It tells you which fact the loop did not establish.

Using the loop variable after the loop

The loop variable i exists only inside the for statement. If you use it after the loop, the compiler stops with an error. Here is a short program with that mistake, and the real message from g++ 15.

#include <iostream>
 
int main() {
    for (int i = 0; i < 3; ++i) {
        std::cout << i << '\n';
    }
    std::cout << "last i = " << i << '\n';
}

Compiler message:

err1.cpp: In function ‘int main()’:
err1.cpp:7:33: error: ‘i’ was not declared in this scope
    7 |     std::cout << "last i = " << i << '\n';
      |                                 ^

If you need the value after the loop, declare the variable before the for statement. The invariant then describes that variable too.

Comparing a signed count with the size of a vector

values.size() returns an unsigned type, which cannot be negative. Comparing it with an int loop variable gives a warning under -Wall. Here is a small program with that loop, and the real output from g++ 15 with -std=c++20 -Wall:

#include <iostream>
#include <vector>
 
int main() {
    std::vector<int> values{4, -7, 12};
    for (int i = 0; i < values.size(); ++i) {
        std::cout << values[i] << '\n';
    }
}

sign_lesson.cpp: In function ‘int main()’:
sign_lesson.cpp:6:23: warning: comparison of integer expressions of different signedness: ‘int’ and ‘std::vector<int>::size_type’ {aka ‘long unsigned int’} [-Wsign-compare]
    6 |     for (int i = 0; i < values.size(); ++i) {
      |                     ~~^~~~~~~~~~~~~~~

Use std::size_t for the index, as the examples above do. The warning is a sign that the types do not match, and a mismatch like this is one of the places where an invariant such as "the index is between 0 and the size" can quietly fail.

Reading a variable that was never set

A variable declared without a value holds whatever bits were in memory. Reading it before setting it is undefined behaviour, which means the program may do anything. In the next program the loop body never runs, so best is never set.

#include <iostream>
#include <vector>
 
int main() {
    std::vector<int> values{4, -7, 12};
    int best;
    for (int i = 0; i < 0; ++i) {
        best = values[i];
    }
    std::cout << "best = " << best << '\n';
}

On one run this printed best = -1481975192; your number will differ. The number is not in the list, and another run could print something else. The invariant "best is one of the values seen" was never established, because no pass ran. Give every variable a value when you declare it, and let the start of the invariant decide that value.

An empty list

values[0] on an empty vector reads past the end of the data, which is undefined behaviour. The check if (values.empty()) in Example 2 is part of the invariant. The start step needs a first value, and an empty list does not have one. Decide what the function returns in that case, and write the check before the loop.

Practice

Exercise 1

Write a loop that multiplies the numbers from 1 to 5 and prints the product. State the invariant after each pass, and check that the final product is correct.

Show the answer

The product is 120. The invariant is: after the pass with counter k, product is the product of the numbers from 1 to k. The start is product = 1, which is the product of an empty list, so the loop must begin with 1, not 0. The keep step multiplies the product by k, which extends the product by one factor. The end is 120 when k reaches 6.

Exercise 2

Here is a loop meant to count how many values in a vector are greater than 10.

int count = 1;
for (std::size_t i = 0; i < values.size(); ++i) {
    if (values[i] > 10) {
        ++count;
    }
}

Find the bug using the invariant.

Show the answer

count starts at 1, which breaks the start step. Before any value is looked at, the count of matching values is 0, so the invariant needs count = 0. The loop counts correctly after that fix, but with the start at 1 the result is always one too large. The fix is to change the declaration to int count = 0;.

Exercise 3

What is the value of total after this loop, and what is the invariant?

int total = 0;
for (int i = 1; i <= 4; ++i) {
    total += i * i;
}

Show the answer

total is 30, because 1 + 4 + 9 + 16 is 30. The invariant is: after the pass with counter i, total is the sum of the squares from 1 squared up to i squared. The start is 0, the sum of an empty list. Each pass adds the next square, which keeps the statement true.

Exercise 4

Write a function int count_negatives(const std::vector<int>& values) that returns how many values are less than 0. Write the invariant as a comment above the loop, then add an assert that checks the count against a second, separate count made with std::count_if. Compile with -std=c++20 -Wall.

Show the answer

One correct version has the invariant "count is the number of negative values in values[0..i-1]". The start is count = 0, which is correct for an empty range. Each pass adds 1 only when the value is negative. The check after the loop compares count with std::count_if(values.begin(), values.end(), [](int x) { return x < 0; }). The two counts must match, so the assert passes for any input list.

Exercise 5

A student writes this function to find the largest value in a vector of integers. It fails for one kind of input. Name the input and explain the failure using the invariant.

int largest(const std::vector<int>& values) {
    int best = 0;
    for (std::size_t i = 0; i < values.size(); ++i) {
        if (values[i] > best) {
            best = values[i];
        }
    }
    return best;
}

Show the answer

The input that fails is any non-empty list where every value is negative, for example {-3, -8}. The function returns 0, which is not in the list. The start best = 0 makes the first part of the invariant false before the loop begins. The fix is int best = values[0]; after an empty check, as in Example 2.

Summary

• A loop invariant is a statement about variables that is true before every pass, and checking it proves the loop.
• Check three things: the start, that each pass keeps the statement true, and what the end of the loop gives you.
• For a sum, the invariant is that the running total equals the sum of the values seen so far. For a maximum, it is that the best value is one of the values seen and is at least all of them.
• A starting value that is not in the data makes the invariant false before the loop begins, and the program prints a wrong answer without warning.
• assert turns the invariant into a check that stops the program when it fails. A check after the loop tests the promise the loop was written to keep.