Chapter 14. Dependent state machines: handling feedback and errors

 

This chapter covers

  • Handling errors in state transitions
  • Developing protocol implementations interactively
  • Guaranteeing security properties in types

As you saw in the previous chapter, you can describe the valid state transitions of a state machine in a dependent type, indexed by the required input state of an operation (its precondition) and the output state (its postcondition). By defining valid state transitions in the type, you can be sure that a program that type-checks is guaranteed to describe a valid sequence of state transitions.

You saw two examples, a description of a door and a simulation of a vending machine, and in each case we gave precise types to the operations to describe how they affected the state. But we didn’t consider the possibility that any of the operations could fail:

  • What if, when you try to open the door, it’s jammed? What if, even though you’ve run the Open operation, it’s still in the DoorClosed state?
  • What if, when you insert a coin in the vending machine, the machine rejects the coin?

In almost any realistic setting, when you try to give precise types to describe a state machine, you’ll need to consider the possibility of the operation failing, or of an unexpected response:

14.1. Dealing with errors in state transitions

14.1.1. Refining the door model: representing failure

14.1.2. A verified, error-checking, door-protocol description

14.2. Security properties in types: modeling an ATM

14.2.1. Defining states for the ATM

14.2.2. Defining a type for the ATM

14.2.3. Simulating an ATM at the console: executing ATMCmd

14.2.4. Refining preconditions using auto-implicits

14.3. A verified guessing game: describing rules in types

14.3.1. Defining an abstract game state and operations

14.3.2. Defining a type for the game state

14.3.3. Implementing the game

14.3.4. Defining a concrete game state

14.3.5. Running the game: executing GameLoop

14.4. Summary