5.4. State Machines 135
ifqandrare consecutive states in the sequence, thenq !r.A state is calledreachableif it appears in some execution.
Definition 5.4.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.^5
(^5) 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.