6.2. State Machines 127
Definition 6.2.4. Thereachable statesof a state machine,M, are defined recur-
sively as follows:
the start state is reachable, and ifpis a reachable state ofM, andp !qis a transition ofM, thenqis
also a reachable state ofM.Definition 6.2.5. Apreserved invariantof a state machine is a predicate,P, on
states, such that wheneverP.q/is true of a state,q, andq !rfor some state,r,
thenP.r/holds.
The Invariant Principle
If a preserved invariant of a state machine is true for the start state,
then it is true for all reachable states.The Invariant Principle is nothing more than the Induction Principle reformulated
in a convenient form for state machines. Showing that a predicate is true in the start
state is the base case of the induction, and showing that a predicate is a preserved
invariant corresponds to the inductive step.^4
(^4) Preserved invariants are commonly just called “invariants” in the literature on program correct-
ness, but we decided to throw in the extra adjective to avoid confusion with other definitions. For
example, other texts (as well as another subject at MIT) use “invariant” to mean “predicate true of
all reachable states.” Let’s call this definition “invariant-2.” Now invariant-2 seems like a reason-
able definition, since unreachable states by definition don’t matter, and all we want to show is that
a desired property is invariant-2. But this confuses theobjectiveof demonstrating that a property is
invariant-2 with themethodof finding apreservedinvariant toshowthat it is invariant-2.