ch:typestate: ch:typestate

Problem and invariant. Check file traces and one branch join. Maintain that every accepted command has a transition from the current state and that a join succeeds only on equal states. The observable result is five named Boolean decisions.

Representation. Use one datatype for absent, open, eof, and closed states and another for the four commands. A transition table stored as triples is easier to extend at run time, but its entries can contain duplicate labels. Pattern matching makes the small frozen automaton total and reviewable.

First complete version. Implement open from absent, both reads from open, and close from open or eof. Fold this partial transition over a list, stopping at the first rejection.

Remaining cases in metatheory order. Add rejection for opening twice, reads outside open, and close outside open or eof. Then compare the final states of two branch results. These are the dynamic cases of state preservation followed by the common-output premise of TS-Read.

A failing version. Return open instead of eof for ReadEof. The mutation still typechecks and audits cleanly; read-after-eof is then accepted and its oracle fails.

Acceptance test. Run the four Appendix E commands. Require the complete trace to pass, all three unavailable operations and the unequal join to be rejected, the exact six-line transcript, and an empty audit. Restore and replay after mutation.

Mathematical boundary. The checker has no heap aliases or procedures. It illustrates theorem 52.4; the finite run does not prove preservation, progress, liveness, or correspondence with a source calculus.