Inductive Verification¶

Why It Matters¶

Many properties must hold over infinite executions or unbounded structures. You can't check all cases directly. Induction lets you handle infinity through two finite proofs: the base and the inductive step. This is how you prove things about loops, recursive structures, and ongoing processes.

The Key Move¶

To prove "property P holds for all N," prove two things: (1) Base case: P holds for N=0 (or the smallest case), and (2) Inductive step: if P holds for N=k (assumption), then P holds for N=k+1. By induction, P holds for all N. The key is finding the right property P - usually an invariant strengthened enough to be inductive.

Classic Application¶

Proving loop invariants. To show a loop maintains invariant I, prove: (1) I holds before the loop starts (base case), and (2) if I holds before an iteration, it holds after (inductive step). Combined with termination, this proves the loop ends with I true - which typically implies the desired postcondition.

Surprising Application¶

Skill development. To prove you can reach expert level from novice, you don't need to map the entire journey. Prove: (1) you can go from zero knowledge to basic competence (base case), and (2) from any skill level, you can improve to the next level through practice (inductive step). By induction, expert level is reachable.

Failure Modes¶

Weak induction hypothesis - P is too weak to prove the inductive step. Strong induction hypothesis - P is too strong, making the base case false. Incorrect induction structure - the right structure might be structural induction (on tree depth) not numerical induction. Non-constructive - proving existence without showing how to compute it.

Go Deeper¶

Manna & Pnueli, "Temporal Verification of Reactive Systems: Safety" (1995); Boyer & Moore, "A Computational Logic Handbook" (1988)