Unit 1.3 · about 4 h
90 / 324Loop invariants, brute-force oracles and differential tests
Stating the invariant first turns debugging into checking. A brute-force oracle plus shrinking turns a wrong program into a minimal counterexample.
- derive
- implement
You can now
- State a loop invariant with initialization, maintenance and termination before coding, following the state-machine pattern.
- Write a Hypothesis differential test that compares an optimized linear routine against a brute-force oracle with controlled seeds.
- Read a shrunken failing input back to the violated invariant.
Covers
- Loop invariants, initialization, maintenance and termination
- Brute-force oracles and randomized differential tests
Study, in this order
5 steps
- Mathematics for Computer Science, Chapter 5, Section 5.4MIT 6.042J - asymptotics and invariants
5.4.1 States and Transitions; 5.4.2 Invariant for a Diagonally-Moving Robot with Lemma 5.4.1 and Theorem 5.4.2; 5.4.3 The Invariant Principle with Definitions 5.4.4 and 5.4.5
Depth · Skim 5.4.4 Die Hard as a second example; skip 5.4.5 Fast Exponentiation.
- Hypothesis QuickstartHypothesis documentation - Quickstart and stateful testing
Write your first test (
@givenwith integers and lists strategies); Running in a test suite; Combining Hypothesis with pytestDepth · Skip the database and shrinking-internals pages; shrinking behavior is used here, not studied.
- Hypothesis: Configuring test settingsHypothesis documentation - Quickstart and stateful testing
Configuring a single test (
@settingswithmax_examples) and the commonly used settings, wherederandomizemakes runs deterministic - Hypothesis stateful testingHypothesis documentation - Quickstart and stateful testing
Rule-based state machines:
rule,preconditionandinvariant;run_state_machine_as_testDepth · Read the rules-and-invariants shape only; full stateful harnesses arrive with Design HashMap in the hash-table unit.
- Sliding window: fixed size (invariant-in-code example)DSA Handbook - Foundations and linear patterns
The pattern (build-first-window then slide) and the four primitives table
Depth · Read only the pattern and primitives as the invariant written in code; the full chapter belongs to the two-pointer unit.
Focus on
- An invariant has three obligations: true at the start, preserved by each step, and strong enough to imply the answer at the end.
- The oracle must be too simple to share the bug: brute force against optimized, with independent code paths.
derandomize(or a fixed seed) makes the run replayable; shrinking then minimizes the failure, which you map back to the invariant clause.- State the invariant in one sentence before the loop; the window primitives show the shape.
Reproduce closed-book
test_window.py comparing the sliding-window max-average against the \(O(nk)\) brute-force oracle with Hypothesis lists of ints in [-100, 100] of length 1 to 30 and \(k\) drawn from 1 to len(nums), max_examples=200, derandomize=True. Run under pytest in Python 3.13 with Hypothesis 6.169.0 and pytest 9.1.1: expect 1 passed. Then break the slide step once (drop the minus term) and confirm the test fails on a shrunken input.Traps
- Testing the optimized code against itself by reusing its helper in the oracle. The oracle shares the bug and everything passes.
- Random tests without seed control: a failure you cannot replay is a rumor, not a regression test.
- Showing maintenance without checking that the invariant implies the postcondition at termination.
Practice
LeetCode 643: Maximum Average Subarray I
Solve with the build-first-window slide. Commit a Hypothesis differential test against the \(O(nk)\) brute force alongside the solution; judge with the worked example nums = [2, 1, 5, 1, 3, 2, 1, 4], \(k = 3\).
After submitting, re-read the handbook sliding-window-fixed worked example and check your trace emits the same running maxima.
Self-test
-
State the Invariant Principle in one sentence.
If a predicate holds initially and every transition preserves it, it holds in all reachable states (Definitions 5.4.4 and 5.4.5). -
Why does the max-average oracle use the \(O(nk)\) double loop instead of a second window implementation?
The double loop recomputes each window from scratch, so it cannot share an off-by-one in the slide update. Independence is what makes disagreement evidence. -
Hypothesis reports a failing input of length 24. What do you do before touching the code?
Let it shrink, replay the minimal case withderandomize, and identify which invariant clause the minimal input violates. -
Write the invariant for the fixed-size window slide.
Before each step, \(s\) equals the sum of the current \(k\) elements. Each step emits the current window and advances by exactly one, so at termination every window was emitted.
Completion criterion
Stop when
Your committed test replays deterministically, catches the seeded minus-term bug, and you can point at the invariant line the shrunken input breaks.
Mark passed, then open 1.4 Only mark this when you can do it without notes.Leads to
- 1.7 Two pointers and sliding windows Window algorithms are the first invariants you will state before coding.
- 1.8 Prefix sums, difference arrays and prefix plus hash Prefix counting is the next brute-force-oracle pattern.
Resources for this unit
- DSA Handbook - Foundations and linear patterns Study Part 0, Part 1, Part 3 and Part 4 in order, plus the Part 5 Linked-list fundamentals chapter. Use the routing-rule pages for arrays versus lists, map choice, stack versus queue, two pointers, sliding windows and prefix methods before seeing solved code.
- MIT 6.042J - asymptotics and invariants Use the asymptotics, state-machine invariants and proof-method readings when a cost or correctness argument is weak. Solve only the matching problems.
- Hypothesis documentation - Quickstart and stateful testing Follow Quickstart for
@givenstrategies and the pytest combination, Configuring test settings formax_examplesandderandomize, then Rule-based state machines (rule,precondition,invariant,run_state_machine_as_test) for randomized operation histories againstdictanddequeoracles.
Also in this section
- AlgoMaster DSA - linear structures slice Attempt Design HashMap, Longest Substring Without Repeating Characters and Sliding Window Maximum cold. Hide tags, state the invariant first, and add randomized operation histories to Design HashMap.
- Algorithms lecture notes - amortized analysis and hashing Use note 9 Amortized Analysis for the summation, taxation, charging and potential-function proofs, and note 5 Hashing for chaining, universal hashing and open-addressing analysis, when the handbook treatment is too brief for a proof.
- Algorithmica - memory and data layout Read the memory hierarchy, cache and complexity-model chapters, then measure one contiguous-versus-linked and one hash-versus-ordered workload crossover.
- NeetCode - unseen linear problems Use only for two tag-hidden transfer problems after the AlgoMaster slice. Do not start another full roadmap or watch a solution before the attempt is complete.
- CPython source - list and dict objects Read
list_resizeinObjects/listobject.cfor the growth formula and pattern comment, and theUSABLE_FRACTIONdefinition, perturbation-probing comment and dummy-entry handling inObjects/dictobject.c. Read the cited functions and comments only.