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: