Teaching Automata Theory and Formal Languages with Dafny
summary
A second‑year automata course encodes textbook definitions in Dafny and produces a machine semantics formalized as a quintuple, a verified imperative simulator that returns acceptance booleans with loop invariants, and a visualizer and web frontend for execution. Students implement DFSMs, debug with the simulator, and construct machine‑specific proofs (induction over string length and state lemmas). Most DFAs/NDFAs and parts of PDAs are fully mechanized; pumping‑lemma and some decidability material remain informal.
AI-written summary · about