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.