primerian.dev
← Fundamentals
Guided lesson 6 questions · 5 languages

Boundaries and loop invariants

What a loop keeps true on every pass, and how empty inputs and the first and last passes expose off-by-one errors.

A loop invariant is a statement that is true before every pass of a loop. It must be true at the start, each pass must keep it true, and when the loop ends it gives the answer. Test a loop by hand at its boundaries: an empty input, one element, and the first and last pass.

Before you begin

Why this matters

Most loop mistakes happen at the edges: the first pass, the last pass, or a list with nothing in it. A loop invariant is one sentence that says what each pass keeps true. With it, you can check a loop with three questions instead of guessing, and you can see at once why a search stops one place early or never stops.

What this helps you reason about

  • State what a loop keeps true, and check it before the first pass, from one pass to the next, and at the end.
  • Spot an off-by-one error by trying an empty input, one element, and the first and last pass.
  • Write a binary search with lo and hi, and explain why it uses lo = mid + 1 and hi = mid.

A school corridor has lockers numbered in order, and a class has quiz marks to add up. Each job is a loop, and each loop is easy to get almost right: one pass too many, one too few, or a list with no marks that nobody tried. This lesson shows how to say what a TypeScript loop keeps true, and how to test it where it usually breaks.

Already know this? The short version
  • A loop invariant is a statement that is true before every pass, such as “total is the sum of the first i marks”: true at the start, kept by each pass, and at the end it gives the answer.
  • Test loops with an empty array, one element, and the first and last pass. In JavaScript, a read past the end gives undefined, and 0 / 0 gives NaN, both without an error.
  • A half-open range [lo, hi) holds hi − lo positions and is empty when lo === hi; a closed range [lo, hi] needs while (lo <= hi) and hi = length − 1.
  • Binary search: lo = 0, hi = length, while (lo < hi), mid = lo + Math.floor((hi - lo) / 2), then lo = mid + 1 or hi = mid. lo = mid can stop shrinking the range, and the loop never ends.
  • Check the invariant at the top of the body with if (…) throw new Error(…).

Go to the final check· Go to the practice tickets

Words in this lesson (6)
loop invariant
A statement about the variables of a loop that is true before every pass, such as “total is the sum of the first i marks”. When the loop ends, the invariant and the condition that ended the loop together give the answer.
boundary
An input at the edge of what a function handles, such as an empty list, a single element, equal values, the first or last element, zero, or a negative number.
off-by-one error
A mistake where a loop or a count goes one step too far or stops one step too early, such as a loop that never reaches the last element of an array.
range
The part of a sequence from a start index up to an end index. The start is included and the end is not, so the range from 1 to 3 holds indexes 1 and 2, and its length is end − start.
binary search
A search in a sorted array that compares with the middle element and keeps only the half that can still hold the value. Each comparison halves what is left.
assertion
A check written into the program that a condition is true at that point. JavaScript has no assert statement: console.assert only prints a message when the condition is false, and a check that must stop the program throws an Error.

Examples are focused snippets; imports, enclosing functions, or classes may be omitted. C examples use C11; Haskell examples use Haskell 2010. Expand the notes for language-specific depth.

01 / Invariant

What stays true while a loop runs?

The marks are in an array: a list of values in order, written [6, 8, 5]. marks[i] is the value at position i, counting from 0, and marks.length is the number of values, as in While loops and termination.

A loop invariant is a statement about the variables of a loop that is true before every pass. It is not the loop condition. The condition decides whether another pass runs; the invariant says what the variables mean each time the condition is tested. In the loop below, the invariant is “total is the sum of the first i marks”.

Check an invariant in three places. At the start: i is 0 and total is 0, and the sum of zero marks is 0, so it is true before the first pass. From one test to the next: if it is true before a pass, the pass adds marks[i] and then adds 1 to i, so it is true again at the next test. Between those two lines it is false for a moment, which is allowed. At the end: the loop stops when i < marks.length is false, so i equals the number of marks, and the invariant now says that total is the sum of all of them. That is the answer the loop was written for.

main.ts
let marks = [6, 8, 5];
let total = 0;
let i = 0;
// invariant: total is the sum of the first i marks
while (i < marks.length) {
  total = total + marks[i];
  i = i + 1;
}
console.log(total); // 19: i is 3, so all 3 marks

A loop invariant is true before the first pass and again before every later pass; when the loop ends, the invariant and the failed condition together give the answer.

Experiment

Check the invariant at every test

The invariant is true at the start, because the sum of zero marks is 0. Each pass adds marks[i] and then adds 1 to i, so it is true again at the next test. When the loop ends, i equals the number of marks, and the invariant says that total is the sum of all of them. Starting total at marks[0] makes the invariant false before the first pass, and nothing in the body repairs it.

Why it matters An invariant that is false before the first pass stays false. Check it with the starting values before you check the body.

Before each test of the condition, predict i and total. Then change let total = 0; to let total = marks[0]; and predict the total printed.

let marks = [6, 8, 5];
let total = 0;
let i = 0;
// total is the sum of the first i marks
while (i < marks.length) {
  total = total + marks[i];
  i = i + 1;
}
console.log("total " + total + ", i " + i);
What to look for

At the while line, i and total show 0 and 0, 1 and 6, 2 and 14, then 3 and 19, and the run prints total 19, i 3. Between the two body lines, total is one mark ahead of i for one stop; this debugger sometimes stops twice on the same line. After the edit, the while line first shows i 0 and total 6, and the extra 6 stays to the end: total 25, i 3.

Expected output

total 19, i 3

02 / Boundaries

Which inputs should you try by hand?

The invariant says what each pass must keep true. A boundary is an input at the edge of what the code handles, and boundaries say where to test the loop by hand. For a loop over a list, try four: an empty list, a list of one element, and the first and the last pass of a longer list.

With an empty list, the loop runs zero times, so the answer is whatever the variables held at the start. For the sum, that is 0, which is right. Code after the loop, or code that reads the first element before the loop, still has to decide what an empty list means.

On the last pass, check every position the body reads, not only i. A loop that counts drops, where a mark is lower than the mark before it, compares marks[i] with marks[i + 1]. Its last pass must be the one where i + 1 is the last position, so the condition is i < marks.length - 1. A condition that lets i reach the last position reads one past the end. Both mistakes are off-by-one errors.

In JavaScript, a read past the end gives undefined, and a comparison with undefined is false, so the drop count happens to come out right. The empty list is the bigger trap. The loop below computes an average. With no marks, total and marks.length are both 0, and 0 / 0 is NaN, as Floating-point numbers showed. Nothing reports an error. Decide what an empty list should show, and test the length before dividing. number[] in the first line says that marks is an array of numbers, so it may also be empty.

main.ts
let marks: number[] = [6, 8, 7];
let total = 0;
for (let i = 0; i < marks.length; i++) {
  total = total + marks[i];
}
if (marks.length > 0) {
  console.log("average " + total / marks.length); // average 7
} else {
  console.log("no marks yet");
}

Test every loop by hand with an empty input, one element, and its first and last pass; on the last pass, check every position the body reads.

Coming from Java or Python: Reading marks[10] in a three-element array does not throw. JavaScript gives undefined, and the loop goes on with it.

Experiment

Average an empty list of marks

An empty array gives zero passes, so total keeps its starting value, 0. Dividing by the length then computes 0 / 0, which is NaN in JavaScript, not an error. The loop is right for an empty array; the line after it is not.

Why it matters Try every loop with an empty input, and decide what the code after the loop should do with zero passes.

Predict the average printed. Then change [6, 8, 7] to [], a pupil with no marks yet, and predict again.

let marks: number[] = [6, 8, 7];
let total = 0;
for (let i = 0; i < marks.length; i++) {
  total = total + marks[i];
}
console.log("average " + total / marks.length);
What to look for

At the total = total + marks[i] line, total shows 0, 6, then 14, and the run prints average 7. After the edit, marks shows [], and the stop after the for line is the console.log line: the body never runs. The run prints average NaN, with no error.

Expected output

average 7

03 / Half-open ranges

Why do half-open ranges avoid off-by-one errors?

For loops and iteration protocols showed that a range includes its start and leaves out its end. A pair of positions lo and hi used this way describes the positions lo, lo + 1, and so on, up to hi − 1. Mathematics writes such a range as [lo, hi): the square bracket means that lo is included, and the round bracket means that hi is not. It is called half-open.

Half-open ranges make three things simple. The number of positions is hi − lo. The range is empty exactly when lo equals hi, so “nothing left” needs no special case. And splitting it at any position mid gives [lo, mid) and [mid, hi), which have no position in common and leave none out.

This makes invariants about ranges easy to state: “everything before lo is below the number we want, everything from hi on is not, and the positions from lo up to hi are not checked yet”. At the start, lo is 0 and hi is the length, so both outer parts are empty, and the statement is true.

The other choice is a closed range, [lo, hi], where hi is included. It holds hi − lo + 1 positions and is empty only when lo is greater than hi. A loop over it runs while (lo <= hi), and a search over it starts with hi = lockers.length - 1. Both choices work. Off-by-one errors come from mixing them: a closed hi with the half-open test lo < hi never looks at position hi, and a half-open hi with the test lo <= hi can read position hi, which may be past the end.

main.ts
// lockers  4   9  15  22  31
// position 0   1   2   3   4
// [1, 4) holds positions 1, 2, 3: hi - lo is 3
// split at mid 2: [1, 2) and [2, 4), no gap, no overlap
// [3, 3) holds nothing: lo == hi

In a half-open range [lo, hi), hi − lo is the number of positions, lo == hi means nothing is left, and splitting at mid gives [lo, mid) and [mid, hi) with no gap and no overlap.

05 / Writing it down

How do you write an invariant down?

Write the invariant above the loop as a comment, so the next reader knows what each pass keeps true. Written as a check, it does more: it stops the program at the first pass where the invariant is false, before a wrong answer reaches the output. Put the check at the top of the body, where the invariant must hold. In TypeScript, write if (the invariant is false) throw new Error("message");. throw stops the program at once with that message, unless code around it catches the error.

A check should be cheap. “Everything before lo is below wanted” would need a loop of its own. Because the lockers are sorted, testing the one locker just before lo is enough: lockers[lo − 1] < wanted. In the same way, lockers[hi] >= wanted covers everything from hi on. The tests lo > 0 and hi < lockers.length are guards, as in Short-circuit evaluation: && skips the read when the position does not exist. A later lesson, Assertions, tests, and counterexamples, uses checks like these in tests.

main.ts
while (lo < hi) {
  // the invariant, checked before each pass
  if (lo > 0 && lockers[lo - 1] >= wanted) {
    throw new Error("lo moved too far");
  }
  if (hi < lockers.length && lockers[hi] < wanted) {
    throw new Error("hi moved too far");
  }
  // ... the search pass, as before
}

Write the invariant above the loop as a comment, and check it at the top of the body, so a broken pass stops the program before a wrong answer is printed.

Precisely: console.assert

console.assert(condition, message) writes the message to the error output when the condition is false, and the program goes on. The stepper shows only standard output, so a failed console.assert is invisible there. A check that must stop the program throws.

Experiment

Let the invariant stop a broken search

The checks test the invariant where it must hold, before each pass. On the first pass, mid is 2 and locker 15 is not below 15, so the correct update is hi = 2. hi = mid - 1 sets hi to 1 and leaves locker 15 behind hi, outside the range. At the next pass, the locker at hi, 9, is below 15, which the invariant forbids, and the check stops the program. Without the checks, the search would go on and print position 1, the locker that holds 9.

Why it matters A checked invariant reports the first pass that breaks it, before a wrong answer reaches the output.

Predict the position printed. Then change hi = mid; to hi = mid - 1; and predict which pass stops the program, and with which message.

let lockers = [4, 9, 15, 22, 31];
let wanted = 15;
let lo = 0;
let hi = lockers.length;
while (lo < hi) {
  // the invariant, checked before each pass
  if (lo > 0 && lockers[lo - 1] >= wanted) {
    throw new Error("lo moved too far");
  }
  if (hi < lockers.length && lockers[hi] < wanted) {
    throw new Error("hi moved too far");
  }
  let mid = lo + Math.floor((hi - lo) / 2);
  if (lockers[mid] < wanted) {
    lo = mid + 1;
  } else {
    hi = mid;
  }
}
console.log("position " + lo);
What to look for

Both checks run at the start of every pass, and neither throws; hi shows 5, then 2, and the run prints position 2. After the edit, the first pass sets hi to 1, and at the next pass the second check finds lockers[1], 9, below 15. The run ends with Error: hi moved too far, and nothing is printed.

Expected output

position 2

06 / Try it

Can you explain a fresh example?

Write down the invariant this loop should keep, and test it before the first pass. Then try a boundary. The next lesson, Function calls, shows how a program runs code that is written somewhere else.

main.ts
let marks = [7, 3, 9, 4];
let below = 0;
let i = 1;
while (i < marks.length) {
  if (marks[i] < 5) {
    below = below + 1;
  }
  i = i + 1;
}
console.log("below 5: " + below);

What is printed? Which mark is never read, and which one-element list gives a wrong count?

Reveal the reasoning

below 5: 2. The loop starts at i = 1, so marks[0], 7, is never read. The invariant should be “below counts the marks below 5 among the first i marks”. Before the first pass, i is 1 and below is 0, so the invariant claims that 7 is not below 5. That happens to be true, so this list gives the right answer by luck. For a list that holds only the mark 3, the loop runs zero times and prints below 5: 0, but 3 is below 5. Start with let i = 0;: then i is 0 and below is 0 before the first pass, and zero marks contain no mark below 5, so the invariant is true for every list.

Practice tickets

  1. INVAR-101 · The class photo app puts some pupils in front of shorter ones → Free
  2. INVAR-102 · The homework app breaks for a pupil with no marks yet → Sign in · Pro
  3. INVAR-103 · The mark band count leaves out pupils on the top mark → Sign in · Pro

Keep exploring

Function calls →

Primary references