# Loop Invariants and Correctness Ideas

Computer Science I · Algorithmics · https://tryals.app/learn/computer-science-i/loop-invariants-and-correctness-ideas

## Proving a Loop Works

Testing shows the presence of bugs; **reasoning** can show their absence. The central tool for arguing an iterative algorithm is correct is the **loop invariant**: a property that is true before the loop starts and remains true after every iteration.

A loop-invariant argument has three parts, mirroring induction:

| Phase | Requirement |
| --- | --- |
| **Initialization** | The invariant is true before the first iteration. |
| **Maintenance** | If true before an iteration, it is still true after. |
| **Termination** | The loop ends, and the invariant implies the result. |

## In Action and Pitfalls

Consider summing a list with a running `total`. The **loop invariant** is "`total` equals the sum of the elements processed so far." It holds initially (`0` elements), is maintained as each step adds the next element, and at termination gives the sum of all elements.

This reasoning catches **off-by-one** and boundary bugs that testing misses.

> **Common pitfall:** Confusing "the loop ran without crashing" with "the loop is correct." Only a well-chosen invariant, shown to hold at initialization and through every iteration, establishes true correctness.

## Practice questions

4 of this lesson's 11 practice questions, with answers. The full set is in the app.

### 1. Order the three parts of a loop-invariant argument, which mirror mathematical induction.

**Answer:**

1. Initialization: the invariant is true before the first iteration
2. Maintenance: if true before an iteration, it stays true after it
3. Termination: the loop ends and the invariant implies the result

**Why:** Initialization, maintenance, termination, the same shape as a proof by induction. Establish the invariant, show every iteration preserves it, and its truth at the end proves the algorithm computed the right thing.

Page: https://tryals.app/practice/computer-science-i/loop-invariants-and-correctness-ideas/order-the-three-parts-of-a-loop-invariant-argument-which-mirror

### 2. A loop invariant proof establishes that *if* the loop terminates, the answer is right. Why is termination a separate obligation, and how is it discharged?

A. Because the invariant already bounds the number of iterations
B. Because an invariant can hold forever in a loop that never exits
C. Because termination follows automatically from a correct invariant
D. Because termination cannot be proved for any loop, by the halting problem

**Answer:** B. Because an invariant can hold forever in a loop that never exits

**Why:** `while true` preserves any invariant you like, so partial correctness and termination are genuinely separate. A decreasing bounded measure, a variant, supplies the second, and it is the same shape as induction. Option 3 overstates the halting problem: no general procedure exists, and particular loops are proved routinely.

Page: https://tryals.app/practice/computer-science-i/loop-invariants-and-correctness-ideas/a-loop-invariant-proof-establishes-that-if-the-loop-terminates-the

### 3. Select every requirement a loop invariant must satisfy to prove an algorithm correct.

A. An invariant proves the loop terminates.
B. Each iteration preserves the invariant.
C. The invariant already holds when execution reaches the loop for the first time.
D. The invariant may be false in the middle of an iteration.
E. The invariant plus the exit condition gives the desired result.

**Answer:** B. Each iteration preserves the invariant.; C. The invariant already holds when execution reaches the loop for the first time.; E. The invariant plus the exit condition gives the desired result.

**Why:** Initialization, maintenance, and a useful termination condition are the three requirements. Running samples and 'never errors' are neither necessary nor sufficient, the whole point is that reasoning, not testing, shows correctness.

Page: https://tryals.app/practice/computer-science-i/loop-invariants-and-correctness-ideas/select-every-requirement-a-loop-invariant-must-satisfy-to-prove-an

### 4. An invariant that holds before the loop and is preserved by each iteration proves the loop correct.

**Answer:** False

**Why:** False. Those two parts give *partial* correctness at best: you also need the exit condition, which combined with the invariant yields the result, and a termination argument showing the loop ends at all. `while true` preserves any invariant you like and proves nothing.

Page: https://tryals.app/practice/computer-science-i/loop-invariants-and-correctness-ideas/an-invariant-that-holds-before-the-loop-and-is-preserved-by-each