Tracing State & Loop Invariants

Overview

A loop invariant is a logical assertion about variable relationships that holds true at the boundary of every iteration — before it starts and after it ends. Tracing state is the practice of manually simulating a loop's execution step-by-step to verify that this assertion is maintained. Together they form the basis of mathematical correctness proofs for iterative algorithms.

Empirical testing via print statements or trial-and-error cannot prove correctness because the space of possible inputs is virtually infinite. A loop invariant, proven via the three phases of initialization, maintenance, and termination, provides a mathematical guarantee analogous to proof by induction.

Where used: Formal software verification tools (Hoare logic) in safety-critical systems like avionics and medical devices, In-place array algorithms: two-pointer duplicate removal where O(1) auxiliary space is guaranteed by the invariant, Google, Flipkart, and Swiggy SDE interviews, which require explicit dry runs across multiple edge cases before coding

Why learn this

It is the only scalable method to prove an algorithm correct — testing covers finite cases, invariants cover all cases.
Top-tier Indian tech interviews (Google L4, Flipkart SDE-1) explicitly require a dry-run trace table before the candidate writes code.
It develops the debugging skill to self-correct base-case and boundary errors without running the code.

Aha moment

# Insertion sort outer loop. Where exactly must the invariant hold?
arr = [5, 2, 4, 6, 1, 3]
for i in range(1, len(arr)):
    key = arr[i]
    j = i - 1
    while j >= 0 and arr[j] > key:  # <-- invariant may be BROKEN here
        arr[j + 1] = arr[j]
        j -= 1
    arr[j + 1] = key  # <-- invariant RESTORED here
print(arr)

Prediction: The invariant arr[0..i-1] is sorted must hold inside the while loop as well.

Common guess: The invariant must hold at all times, including inside the inner while loop.

The invariant only needs to hold at the START of each outer for-loop iteration. Inside the inner while loop, elements are actively being shifted — the subarray is temporarily unsorted. The invariant is restored only after arr[j+1] = key places the element in its correct position. This is why mid-loop validation is a conceptual error.

Common mistakes

Validating the invariant mid-iteration: Invariants are only required to hold at the strict boundaries — at the exact start and exact end of each iteration. Inside the loop body, state is actively being mutated and the invariant may be temporarily false. Checking it mid-loop leads to incorrect conclusions about correctness.
Forgetting to verify the termination condition: An invariant can be perfectly maintained across every iteration and yet the algorithm never halts if the loop's exit condition is never triggered. Both the invariant and the progress toward termination must be verified independently.
Relying on an IDE or auto-judge instead of manual tracing: Failing edge cases (empty arrays, single elements, negative boundaries) during interviews is almost always a failure to validate the initialization phase of the invariant. Manual state tracing catches these before any code is run.

Glossary

logical assertion: A mathematical statement or rule that claims to be absolutely true at a specific moment.
proof by induction: A mathematical way of proving something works for every step by proving the first step and the transition to the next.
dry-run trace table: Manually acting like a computer on paper, tracking every variable's value as the code runs.

Recall questions

What are the three phases required to prove a loop invariant, and what mathematical technique do they mirror?
State the loop invariant for Insertion Sort's outer loop.
Why is an invariant only required to hold at iteration boundaries, not inside the loop body?

Understanding checks

What does this code print, and what is the loop invariant that guarantees the result is correct?

It prints [1, 2, 3]. The invariant is: at the start of each iteration, arr[0..write-1] contains exactly the unique elements seen so far, in their original order.

Understanding the invariant explains why overwriting arr[write] is safe — everything behind the write pointer is already finalized and unique. This is the O(1) auxiliary space guarantee.

A loop's invariant is verified to hold at initialization and is proven to be maintained across every iteration, yet the program times out. What is the most likely cause, and which phase of the invariant proof does it correspond to?

The loop's exit condition is never triggered — the state variables never make progress toward terminating the loop. This corresponds to a failure of the Termination phase of the invariant proof.

Maintenance guarantees the invariant persists, but it says nothing about convergence. The termination phase must separately prove that each iteration moves the loop closer to its exit condition.

Practice tasks

Prove the two-pointer invariant for LeetCode 26

The starter code solves LeetCode 26 (Remove Duplicates from Sorted Array). Add comments that explicitly state the invariant, then write a dry-run trace table for the input [1, 1, 2, 3, 3] showing the value of 'write' and arr[:write] at the START of each iteration (boundary only, not mid-loop).

Continue learning

Previous: What is an Algorithm?

Next: Iteration & Traversal

Return to DSA Roadmap