Chapter 13. State machines: verifying protocols in types

 

This chapter covers

  • Specifying protocols in types
  • Describing preconditions and postconditions of operations
  • Using dependent types in state

In the previous chapter, you saw how to manage mutable state by defining a type for representing sequences of commands in a system, and a function for running those commands. This follows a common pattern: the data type describes a sequence of operations, and the function interprets that sequence in a particular context. For example, State describes sequences of stateful operations, and runState interprets those operations with a specific initial state.

In this chapter, we’ll look at one of the advantages of using a type for describing sequences of operations and keeping the execution function separate. It allows you to make the descriptions more precise, so that certain operations can only be run when the state has a specific form. For example, some operations require access to a resource, such as a file handle or database connection, before they’re executed:

  • You need an open file handle to read from a file successfully.
  • You need a connection to a database before you can run a query on the database.

13.1. State machines: tracking state in types

13.1.1. Finite state machines: modeling a door as a type

13.1.2. Interactive development of sequences of door operations

13.1.3. Infinite states: modeling a vending machine

13.1.4. A verified vending machine description

13.2. Dependent types in state: implementing a stack

13.2.1. Representing stack operations in a state machine

13.2.2. Implementing the stack using Vect

13.2.3. Using a stack interactively: a stack-based calculator

13.3. Summary