Identifying Correctness Invariants in Algorithms

Good to see you again. Last time, you focused on making Java comparators safe and precise: ordering is a logical policy, not subtraction that happens to work on ordinary values. The same discipline applies here. An algorithm is not correct because it “looks standard”; it is correct because a precise claim remains true throughout its execution.

This lesson builds the interview-ready skill of stating that claim: an invariant. You will learn to formulate invariants for loops and recursive helpers, check them through initialization, maintenance, and exit, and use them to explain why a solution works without turning an interview explanation into a formal-methods lecture.

---

What an invariant says

A loop invariant is a statement that is true every time the loop guard is evaluated: before the first iteration, before each later iteration, and when the guard finally becomes false.

The most useful invariants describe the relationship between:

• progress variables, such as i, left, right, or a write pointer;
• the work already completed;
• the work that remains; and
• an accumulated answer, candidate region, or partially arranged data structure.

For an array scan, use the half-open range notation $a[0,i)$ to mean indices from $0$ up to but excluding $i$. At the beginning of an iteration where i == 4, the prefix $a[0,4)$ contains the four elements already processed; a[4] is the next one.

For example:

static int countOccurrences(int[] nums, int key) {
    int count = 0;

    /*
     * Invariant:
     * 1. 0 <= i && i <= nums.length
     * 2. count equals the number of occurrences of key in nums[0..i).
     */
    for (int i = 0; i < nums.length; i++) {
        if (nums[i] == key) {
            count++;
        }
    }

    return count;
}

The invariant is not merely “i increases” or “count is nonnegative.” Those facts may be true, but they do not explain why count is the right answer. The important statement connects count to exactly the prefix examined so far.

The Cornell CS 2112 reading gives a compact formal definition and then uses invariants to justify a binary-search implementation. Read its proof framework now; it will give you the vocabulary used in the rest of this lesson.

---

The correctness framework: preserve a useful truth

A loop invariant is useful only when it supports a complete correctness argument. The central flowchart is worth keeping in mind:

For interview purposes, use this four-part structure:

1. Initialization: The invariant holds before the first guard check.
2. Maintenance: Assume it holds at the start of one iteration. Show that the body restores it before the next guard check.
3. Exit reasoning: Combine “the invariant holds” with “the guard is false” to obtain the postcondition.
4. Progress: Identify a bounded quantity that moves toward termination.

The first three establish partial correctness: if the algorithm stops, its answer is correct. The fourth establishes that it does stop.

Watch the invariant-proof overview and its linear-search example from Algorithms Lab. The example is especially valuable because its invariant describes the remaining possible location of the target, rather than an answer accumulated so far.

A subtle but important point

The invariant need not be true after every individual line inside the loop body. It must be true at the points where the next iteration could begin.

In countOccurrences, suppose nums[i] == key. Right after count++, but before i++, the written invariant is temporarily inaccurate: count reflects the prefix through index i, while i still identifies the old prefix boundary. Once the for loop increment executes, the relationship is restored.

This gives a reliable way to inspect update order:

Ask: after all updates for this iteration, does every variable again describe the same processed region?

---

Example 1: a scan invariant

Consider a maximum-value scan. Assume nums is nonempty.

static int maxValue(int[] nums) {
    int best = nums[0];

    /*
     * Invariant:
     * 1. 1 <= i && i <= nums.length
     * 2. best is the maximum value in nums[0..i).
     */
    for (int i = 1; i < nums.length; i++) {
        if (nums[i] > best) {
            best = nums[i];
        }
    }

    return best;
}

Here is the correctness explanation you should be able to say aloud.

Initialization. Initially, i == 1 and best == nums[0]. The range nums[0..1) contains only nums[0], so best is its maximum.

Maintenance. Assume best is the maximum of nums[0..i). The next element is nums[i].

• If nums[i] exceeds best, assigning it to best makes best the maximum of nums[0..i+1).
• Otherwise, the old best is still the maximum after including nums[i].

After the loop increment, i has become i + 1, so the invariant is restored.

Exit reasoning. The loop exits when i == nums.length. The invariant then says best is the maximum in nums[0..nums.length), which is the entire array.

Progress. The remaining unprocessed elements, nums.length - i, decrease by one per iteration and cannot become negative while the guard holds.

Notice how the invariant directly exposes an initialization requirement. If you instead wrote:

int best = 0;

the invariant would fail for an array containing only negative numbers. This is why invariants are a debugging tool, not just proof decoration.

A compact scan template

When one pointer scans from left to right, start with this sentence:

“At the beginning of each iteration, answer correctly summarizes the elements in the processed prefix, and i is the first unprocessed index.”

Then make “summarizes” specific:

Problem type	Typical invariant
Count matches	count is the number of matches in the processed prefix.
Running sum	sum equals the sum of the processed prefix.
Best value	best is the maximum or minimum in the processed prefix.
First valid index	No earlier index in the processed prefix satisfies the target condition.
Frequency map	The map contains exactly the frequencies of values in the processed prefix.

“best is the best value seen so far” is acceptable conversational shorthand, but in a proof-quality explanation, say best over which range.

---

Example 2: two pointers preserve a candidate region

In later array problems, a common pattern uses two pointers in a sorted array to find two distinct values whose sum equals target.

static boolean hasPairWithSum(int[] nums, int target) {
    int left = 0;
    int right = nums.length - 1;

    /*
     * Preconditions: nums is sorted in nondecreasing order.
     *
     * Invariant:
     * 1. 0 <= left <= right + 1 <= nums.length
     * 2. If a valid distinct-index pair with sum target exists and has not
     *    already been returned, then some valid pair uses two indices in
     *    the current range [left..right].
     */
    while (left < right) {
        long sum = (long) nums[left] + nums[right];

        if (sum == target) {
            return true;
        } else if (sum < target) {
            left++;
        } else {
            right--;
        }
    }

    return false;
}

This is a candidate-region invariant. The active interval contains every solution that has not already been found.

Why moving left is safe

Suppose the current sum is less than target:

$$\text{nums[left]}+\text{nums[right]}<\text{target}$$

Because the array is sorted, nums[right] is the largest value currently available to pair with nums[left]. Any other candidate index $j$ with $left<j\le right$ satisfies:

$$\text{nums[left]}+\text{nums[j]}\le \text{nums[left]}+\text{nums[right]}<\text{target}$$

So left cannot participate in a valid pair in the current candidate region. Incrementing left discards no solution.

The argument for sum > target is symmetric: nums[left] is the smallest available partner for nums[right]. If even that sum is too large, right cannot appear in a solution, so decrementing right is safe.

At exit, left >= right. The candidate region contains at most one index, so it cannot contain a pair of distinct indices. The invariant says every possible solution would have had to remain in that region. Therefore, no valid pair exists.

Two details are worth carrying into interviews:

• The invariant requires the array’s sortedness. It is not a background detail; it is what makes discarding an endpoint valid.
• Use long sum when nums and target are int values, because adding two int values can overflow before comparison.

For narrowing algorithms, this is the recurring idea:

State what remains possible, then justify why each branch removes only impossible candidates.

That same form will reappear in binary search, feasibility searches, and some graph algorithms.

---

How to construct an invariant under interview pressure

Do not try to invent formal language after coding. Derive the invariant before, or while, writing the loop.

1. State the desired postcondition

Be precise about what must be true at return.

Examples:

• “count equals the number of target occurrences in the whole array.”
• “All elements before write are nonzero and preserve their original order.”
• “Any answer still possible lies between left and right.”
• “The output prefix contains the smallest values among the consumed input prefixes.”

2. Freeze the algorithm midway

Imagine the loop paused just before its guard is evaluated. Divide the data into regions:

• processed versus unprocessed;
• known-good left region, unknown middle region, known-good right region;
• discarded candidate region versus remaining candidate region.

Then ask: what does each variable mean at that instant?

3. Generalize the postcondition to the partial state

If the final desired claim is “best is the maximum of the whole array,” the midway claim becomes “best is the maximum of the processed prefix.”

If the final claim is “all values are partitioned,” the midway claim becomes “the regions already claimed by each pointer have the required property; only the middle remains unresolved.”

4. Check exit reasoning early

Combine your proposed invariant with a false guard. Does the required result follow?

If not, the invariant is too weak.

For example, “left and right remain in bounds” is true for a two-pointer search but says nothing about whether a target pair might have been discarded. It cannot prove false is correct at loop exit.

5. Test initialization and each branch

If you cannot make the invariant true at the start, it is too strong or your initialization is wrong. If one branch cannot restore it, either the branch is invalid or the invariant omits a needed condition.

This is also why a good invariant naturally leads to clean code: the update rules are chosen to re-establish the statement.

---

Recursive algorithms: state the call contract

For recursion, use nearly the same reasoning, but phrase the invariant as a contract for every recursive call.

Consider summing a specified half-open range.

static long rangeSum(int[] nums, int lo, int hi) {
    /*
     * Contract:
     * - Requires: 0 <= lo && lo <= hi && hi <= nums.length
     * - Returns the sum of nums[lo..hi).
     */
    if (lo == hi) {
        return 0L;
    }

    return nums[lo] + rangeSum(nums, lo + 1, hi);
}

The recursive invariant, or call contract, is:

For every invocation with valid bounds, rangeSum(nums, lo, hi) returns the sum of exactly the elements in $nums[lo,hi)$.

The proof mirrors a loop proof:

• Base case: When lo == hi, the range is empty, and its sum is 0.
• Recursive maintenance: If the recursive call correctly sums $nums[lo+1,hi)$, adding nums[lo] produces the sum of $nums[lo,hi)$.
• Progress: The range length $hi-lo$ decreases by one on every call, so the base case is eventually reached.

For a tail-recursive helper, the relationship is even more direct. This helper has the same invariant as the iterative counting loop:

static int countKey(int[] nums, int i, int count, int key) {
    /*
     * Requires:
     * - 0 <= i && i <= nums.length
     * - count is the number of occurrences of key in nums[0..i).
     */
    if (i == nums.length) {
        return count;
    }

    int nextCount = count + (nums[i] == key ? 1 : 0);
    return countKey(nums, i + 1, nextCount, key);
}

Each recursive call must satisfy the helper’s precondition. That precondition is the recursive equivalent of the loop invariant. At the base case, i == nums.length, so the claim about the processed prefix becomes a claim about the entire array.

Java does not guarantee tail-call optimization, so this recursive version is a reasoning aid rather than the preferred implementation for a large array. The iterative version uses constant auxiliary space; the recursive version can use one stack frame per element.

Recursive-proof speaking template

For ordinary interview recursion, a concise explanation is enough:

“Define the function so that it returns the correct answer for the subproblem represented by its parameters. The base case is correct directly. Each recursive call receives a strictly smaller valid subproblem. Assuming those calls return correct answers, the current call combines them correctly.”

That is induction in practical form. You do not need to announce “proof by induction” unless the interviewer asks for a formal proof.

---

A practical invariant checklist

Before submitting a loop-heavy solution, spend about 30 seconds on this checklist:

• Scope: Which loop or recursive helper does this invariant describe?
• Timing: Is it true whenever the loop guard is evaluated, or at the entry to every recursive call?
• Regions: Which elements have been processed, and which remain?
• Meaning: What does each accumulator, pointer, map, stack, or heap represent?
• Initialization: Does the empty or initial region make the statement true?
• Maintenance: Does every branch re-establish the statement?
• Exit: Does the false guard, together with the invariant, imply the required answer?
• Progress: What bounded quantity changes so execution ends?

During practice, add a one- or two-line invariant comment above each nontrivial loop before you code its body. The goal is not to write lengthy proofs for every easy problem. It is to make the key fact explicit enough that off-by-one errors, unsafe pointer moves, and missing state updates become visible before submission.

---

Key takeaways

An invariant is the precise statement that remains true at each loop boundary or recursive-call boundary and explains why the algorithm can safely make progress.

For loops, justify correctness through:

1. initialization;
2. maintenance;
3. exit reasoning; and
4. a progress measure for termination.

The most reusable interview invariant forms are:

• an accumulator correctly summarizes a processed prefix;
• a candidate region still contains every possible unanswered solution; and
• established regions of an in-place structure already satisfy their required properties.

For recursion, state a contract that holds for every valid call, prove the base case directly, show recursive calls receive smaller valid subproblems, and explain how their results are combined.

Next, you will turn this reasoning into a concrete submission habit: constructing boundary and adversarial test cases that expose incorrect initialization, branch logic, and termination conditions.