Specifications are more expressive than code. This comes at a cost: it’s not always clear how to go from a specification to reality. A technique for handling this is to write a very abstract spec and expand it into a more detailed, lower-level “implementation” that is closer to the program you’ll be writing. One very common pattern for doing this is to use a state machine. In this chapter, we will learn how to represent them and use them in writing our specifications.
State Machines
A state machine is a system with a finite set of internal “states” along with a set of transitions between the states. Outside ...
