Inspiration: CS61BL Lab 14 — Topological Sort, "Discussion: Topological Sorts and DAG's" (cs61bl.org/labs/lab14) — implementing
path(start, stop)
A tempting way to implement path(start, stop): run a DFS from start, record vertices in visit order, truncate at stop, and return that list. It compiles, and on small graphs it may even pass.
But consider a graph with a dead-end branch: edges 5→2, 2→1, 5→4, 4→0, and query path(5, 0). DFS visits [5, 2, 1, 4, 0] — it dives into the dead end 2→1 first, backtracks, then finds the real route. There is no edge between 1 and 4. The visit order is a traversal order, not a walk: consecutive entries are not guaranteed to be adjacent.
So the raw sequence must be pruned. The natural worry then becomes: when pruning, might we ever need to insert a vertex that isn't in the sequence? The answer is no — and the reason is a small lemma worth remembering on its own.
Lemma (DFS predecessor property). Let v₀, v₁, …, vₖ be the DFS visit order starting from start (so v₀ = start). Then for every i > 0, there exists j < i such that the edge vⱼ → vᵢ exists.
Proof (one sentence). A vertex is pushed onto the fringe only as a neighbor of some already-visited vertex, and "already visited" means "appears earlier in the sequence." ∎
In other words: no vertex in a DFS sequence appears out of nowhere — every vertex owes an incoming edge to someone earlier.
Corollary. The DFS visit order (truncated at stop) contains a valid start → stop path as a subsequence. Path reconstruction therefore only ever removes vertices — it never needs to add one.
Two guarantees combine to make this safe:
i, scanning left always finds at least one j with vⱼ → vᵢ. The backward walk can never get stuck at a vertex with no in-sequence predecessor.v₀ = start (every other vertex has a predecessor to jump to).The legal path was hiding in the sequence all along; reconstruction is pure subtraction.
path[j] is adjacent to path[i] for some j < i, delete everything strictly between them, then continue from j. The deleted region sits strictly between two vertices already confirmed to stay, so connectivity is preserved by construction.stop, repeatedly scan left for any earlier with isAdjacent(earlier, current), jump there, repeat until start, then reverse. One loop with an inner scan — no index bookkeeping over a mutating list.Both are correct for the same reason: the lemma.