Typestate and State-Transition Protocols

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

A program may own a file handle exactly once and still execute $\mathsf{read}$ after $\mathsf{close}$. Ownership controls aliases; it does not say which operations are available in the handle’s current state. The missing datum is a state that changes when an operation succeeds.

The file protocol

Let the protocol states be $$Q=\{\mathsf{open},\mathsf{eof},\mathsf{closed}\}.$$ A protocol transition is a labeled edge $q\stackrel{a}{\to }{q}^{\prime }$ between states. The file automaton has There is no outgoing read edge from $\mathsf{eof}$ or $\mathsf{closed}$, and there is no outgoing close edge from $\mathsf{closed}$. These absences, rather than run-time tests inserted by the type system, reject the two protocol errors.

The distinction between a state and a type index is exact. The run-time map $H$ stores $H(\ell )=q$ for a concrete handle identity $\ell$. The static context stores $f:\mathsf{File}[q]$. A value environment $\eta$ maps $f$ to $\ell$. We write $$H,\eta {\vDash }_{\mathsf{ts}}\mathrm{\Delta }$$ if and only if every $f:\mathsf{File}[q]\in \mathrm{\Delta }$ has a distinct $\eta (f)=\ell$ and $H(\ell )=q$. Distinctness is the alias restriction. This is the sole-handle pattern of chapter 19 instantiated with a file: ownership supplies the non-aliasing fact, while the index $q$ adds the operation-availability invariant that ownership alone lacks.

Commands and flow-sensitive typing

Programs are in administrative form: where $X$ ranges over declared protocol procedures. The flow judgment $$\mathrm{\Delta }⊢P⊣{\mathrm{\Delta }}^{\prime }$$ means that $P$ consumes the handles in $\mathrm{\Delta }$ according to their states and, if it returns, leaves exactly ${\mathrm{\Delta }}^{\prime }$. The principal rules are

$\mathrm{\Delta }⊢\mathsf{return}⊣\mathrm{\Delta }$

$\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]⊢P⊣{\mathrm{\Delta }}^{\prime }$$f\notin \mathrm{dom}(\mathrm{\Delta })$

$\mathrm{\Delta }⊢\mathsf{open}f;P⊣{\mathrm{\Delta }}^{\prime }$

$q\in \{\mathsf{open},\mathsf{eof}\}$$\mathrm{\Delta }⊢P⊣{\mathrm{\Delta }}^{\prime }$

$\mathrm{\Delta },f:\mathsf{File}[q]⊢\mathsf{close}f;P⊣{\mathrm{\Delta }}^{\prime }$

$\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]⊢P_m⊣{\mathrm{\Delta }}^{\prime }$$\mathrm{\Delta },f:\mathsf{File}[\mathsf{eof}]⊢P_e⊣{\mathrm{\Delta }}^{\prime }$

$\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]⊢\mathsf{read}f\mathsf{as}\{\mathsf{more}(f)\Rightarrow P_m\mid \mathsf{eof}(f)\Rightarrow P_e\}⊣{\mathrm{\Delta }}^{\prime }$

The two read branches start with different state indices but must finish in the same context ${\mathrm{\Delta }}^{\prime }$. This is the join condition. Taking the union of the two contexts would be unsound: a handle closed on one branch and open on the other would then appear available after the join.

Fix a procedure table $\mathrm{\Omega }$. Its entries have the form $X:(x:\mathsf{File}[q])⊸{\mathrm{\Delta }}_X=P_X$, where $x$ may occur in the output context. To keep this first-order interface closed, $\mathrm{dom}({\mathrm{\Delta }}_X)\subseteq \{x\}$; a handle opened inside $P_X$ must be closed before the procedure returns. The table is suppressed in the flow judgment. Its call rule is $$\frac{X:(x:\mathsf{File}[q])⊸{\mathrm{\Delta }}_X=P_X\in \mathrm{\Omega }}{f:\mathsf{File}[q]⊢X(f)⊣{\mathrm{\Delta }}_X[f/x]}\mathrm{TS}-\mathrm{Call}.$$ A recursive table is admitted only after every declared body checks from its declared input to its declared output while calls use the assumed table. The rule therefore unfolds a previously checked body; it does not infer a recursive invariant.

The following program closes the file on every returning path: Its checked signatures are $$\mathsf{drain}:\mathsf{File}[\mathsf{open}]⊸\varnothing ,\varnothing ⊢\mathsf{main}⊣\varnothing .$$ The recursive branch re-establishes the exact input state of $\mathsf{drain}$. The eof branch consumes the handle. Thus both branches join at the empty context.

Operational transitions

A configuration is $⟨H,\eta ,P⟩$. Opening chooses a handle $\ell \notin \mathrm{dom}(H)$. Closing removes the handle from $H$ and its variable from $\eta$. A read step consults an external reply $b\in \{\mathsf{more},\mathsf{eof}\}$:

$\ell \notin \mathrm{dom}(H)$

$⟨H,\eta ,\mathsf{open}f;P⟩{⟶}_{\mathsf{ts}}⟨H[\ell \mapsto \mathsf{open}],\eta [f\mapsto \ell ],P⟩$

$\eta (f)=\ell$$H(\ell )\in \{\mathsf{open},\mathsf{eof}\}$

$⟨H,\eta ,\mathsf{close}f;P⟩{⟶}_{\mathsf{ts}}⟨H\setminus \ell ,\eta \setminus f,P⟩$

$\eta (f)=\ell$$H(\ell )=\mathsf{open}$

$⟨H,\eta ,\mathsf{read}f\mathsf{as}\{P_m\mid P_e\}⟩{⟶}_{\mathsf{ts}}⟨H,\eta ,P_m⟩$

$\eta (f)=\ell$$H(\ell )=\mathsf{open}$

$⟨H,\eta ,\mathsf{read}f\mathsf{as}\{P_m\mid P_e\}⟩{⟶}_{\mathsf{ts}}⟨H[\ell \mapsto \mathsf{eof}],\eta ,P_e⟩$

The abbreviated branch syntax in the dynamics keeps the same binder $f$ in each continuation. Procedure calls use $$\frac{X:(x:\mathsf{File}[q])⊸{\mathrm{\Delta }}_X=P_X\in \mathrm{\Omega }}{⟨H,\eta ,X(f)⟩{⟶}_{\mathsf{ts}}⟨H,\eta ,P_X[f/x]⟩}\mathrm{TSO}-\mathrm{Call}$$ Before this rule is used, every procedure-local handle binder is alpha-renamed fresh for $H$, $\eta$, and the caller; the displayed substitution then renames the formal handle to $f$.

Let $D_f$ abbreviate the displayed body of $\mathsf{drain}(f)$. For an input consisting of one chunk followed by eof, the complete trace is Every relation is one step. The final configuration has no live handle.

The state invariant

Proof of Lemma 52.2 — One-step state preservation

Proof. Induct on the dynamic step. For TSO-Open, the fresh identity $\ell$ extends both maps and TS-Open’s premise supplies the continuation derivation; take ${\mathrm{\Delta }}_1=\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]$. For TSO-Close, agreement gives the state $q$ required by TS-Close; removing $\ell$, $f$, and their unique correspondence leaves agreement with the rule’s premise context $\mathrm{\Delta }$.

For TSO-Read-More, take ${\mathrm{\Delta }}_1=\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]$ and use the first TS-Read premise. For TSO-Read-Eof, update the one agreeing heap entry to $\mathsf{eof}$, take ${\mathrm{\Delta }}_1=\mathrm{\Delta },f:\mathsf{File}[\mathsf{eof}]$, and use the second premise. Procedure unfolding uses the checked declaration and renames its formal handle to $f$; the injectivity clause of agreement is unchanged. These are all dynamic rules. ◻

Proof of Lemma 52.3 — Protocol progress

Proof. Invert the last typing rule. TS-Return gives the first alternative. For TS-Open, choose an identity outside the finite domain of $H$. For TS-Close, agreement provides the concrete identity and exact state, so TSO-Close applies. For TS-Read, agreement gives an open heap entry; the external reply selects one of the two read rules. A procedure call unfolds because every admitted signature has a checked body. ◻

Proof of Theorem 52.4 — Protocol safety

Proof. Induct on the length of the reduction. The zero-step case is the initial agreement. For a successor length, apply lemma 52.2 to obtain the typed agreeing successor configuration, then apply the induction hypothesis. Every read or close step uses a dynamic premise matching an edge printed in section 52.1; progress shows that a well-typed command is never blocked by a missing edge. At $\mathsf{return}$, the flow judgment is TS-Return, so its input context is ${\mathrm{\Delta }}_f$, and the maintained agreement gives the final claim. ◻

The theorem depends on affine handle identity. If agreement allowed $\eta (f)=\eta (g)=\ell$, one alias could close $\ell$ while the other retained type $\mathsf{File}[\mathsf{open}]$; the next read would refute preservation.

Encodings and theorem boundaries

Sources.

Strom and Yemini’s archived PDF page 3 (printed page 159) defines typestates, operation preconditions, and operation-dependent poststates [SY86]. Modern modular systems combine protocol states with access permissions so that aliases cannot invalidate a state guarantee; the archived modular-typestate PDF pages 8 and 10 print the input stream automaton, permissions, and branching read postcondition [BA07]. Featherweight Typestate makes state change a primitive language operation: its archived PDF pages 4–5 print the file automaton and aliasing counterexample, and pages 21 and 33 state progress and preservation for the static and gradual calculi [GTWA14]. The finite kernel in this chapter is book-owned; its preceding proof does not claim to be a translation of any of those richer object calculi.

A sum-type encoding returns $\mathsf{File}[\mathsf{open}]\oplus \mathsf{File}[\mathsf{eof}]$ from read. It accounts for branching but needs the same affine elimination discipline to prevent duplication. A binary session type coordinates dual communicating endpoints; the file kernel has one local resource and therefore proves no duality, communication fidelity, or deadlock freedom. Affine typestate combines the two independent obligations visible here: a state index selects the available edge, and affinity prevents a stale alias.

Protocol safety is a safety property. The external source may return $\mathsf{more}$ forever, so $\mathsf{drain}$ may diverge. Nothing in theorem 52.4 proves termination, eventual close, or temporal liveness.