Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

How to Verify a Turing Machine with Dafny

Edgar F. A. Lederer

TL;DR

This work demonstrates rigorous, machine-checked verification of two classic Turing machines in Dafny, establishing total correctness for each decider and illustrating the feasibility of formal proofs for teaching-oriented TM models. The author develops detailed invariants and termination metrics, including a left-minus-right invariant and a never-more invariant for the parentheses machine, and a halving/power-of-two invariant for Sipser’s M2, to drive complete partial and total correctness proofs. Beyond the specific machines, the paper showcases a practical methodology for mechanized TM verification, including ghost state, auxiliary lemmas, and structured stepwise proofs that reveal the interplay between tape content, head position, and input word properties. The work argues that mechanized proof not only certifies correctness but deepens understanding, and positions Dafny as a suitable tool for formalizing basic theoretical constructs used in computer science education. The contributions thus bridge pedagogy and formal verification, yielding compact, executable specifications and verifiable proofs that illuminate TM behavior with precise invariants and termination arguments.

Abstract

This paper describes the formal verification of two Turing machines using the program verifier Dafny. Both machines are deciders, so we prove total correctness. They are typical first examples of Turing machines used in any course of Theoretical Computer Science; in fact, the second machine is literally taken from a relevant textbook. Usually, the correctness of such machines is made plausible by some informal explanations of their basic ideas, augmented with a few sample executions, but neither by rigorous mathematical nor mechanized formal proof. No wonder: The invariants (and variants) required for such proofs are big artifacts, peppered with overpowering technical details. Finding and checking these artifacts without mechanical support is practically impossible, and such support is only available since recent times. But nowadays, just because of these technicalities, with such subjects under proof a program verifier can really show off and demonstrate its capabilities.

How to Verify a Turing Machine with Dafny

TL;DR

This work demonstrates rigorous, machine-checked verification of two classic Turing machines in Dafny, establishing total correctness for each decider and illustrating the feasibility of formal proofs for teaching-oriented TM models. The author develops detailed invariants and termination metrics, including a left-minus-right invariant and a never-more invariant for the parentheses machine, and a halving/power-of-two invariant for Sipser’s M2, to drive complete partial and total correctness proofs. Beyond the specific machines, the paper showcases a practical methodology for mechanized TM verification, including ghost state, auxiliary lemmas, and structured stepwise proofs that reveal the interplay between tape content, head position, and input word properties. The work argues that mechanized proof not only certifies correctness but deepens understanding, and positions Dafny as a suitable tool for formalizing basic theoretical constructs used in computer science education. The contributions thus bridge pedagogy and formal verification, yielding compact, executable specifications and verifiable proofs that illuminate TM behavior with precise invariants and termination arguments.

Abstract

This paper describes the formal verification of two Turing machines using the program verifier Dafny. Both machines are deciders, so we prove total correctness. They are typical first examples of Turing machines used in any course of Theoretical Computer Science; in fact, the second machine is literally taken from a relevant textbook. Usually, the correctness of such machines is made plausible by some informal explanations of their basic ideas, augmented with a few sample executions, but neither by rigorous mathematical nor mechanized formal proof. No wonder: The invariants (and variants) required for such proofs are big artifacts, peppered with overpowering technical details. Finding and checking these artifacts without mechanical support is practically impossible, and such support is only available since recent times. But nowadays, just because of these technicalities, with such subjects under proof a program verifier can really show off and demonstrate its capabilities.
Paper Structure (55 sections, 2 theorems, 49 equations, 8 figures)

This paper contains 55 sections, 2 theorems, 49 equations, 8 figures.

Table of Contents

  1. Introduction
  2. The Turing Machine Model
  3. Task
  4. Machine
  5. Computation
  6. How 'infinite' is the tape?
  7. The First Example Machine: Parentheses
  8. The Language
  9. The Machine
  10. Working of the machine --- informally
  11. How 'finite' is the tape?
  12. Implementation
  13. Verification
  14. Global and local invariants
  15. Our proceeding
  16. ...and 40 more sections

Key Result

Lemma 1

Let $T$ be a type, $k$ a variable of type $T$, $C$ a command that does not assign to $k$, and $Q$ a predicate in which $k$ may occur as a free variable, but no others. Then $\Box$

Figures (8)

  • Figure 1: First Turing machine --- Parentheses.
  • Figure 2: High-level view onto the computation.
  • Figure 3: Low-level view onto the computation.
  • Figure 4: Second Turing machine --- Powers of two (Sipser's $M_2$).
  • Figure 5: Division by two --- the local invariants for $q_1$.
  • ...and 3 more figures

Theorems & Definitions (7)

  • Lemma 1: Generalized Skip Lemma
  • Remark 2
  • Proof 3
  • Lemma 4: Accumulated Invariant Lemma
  • Remark 5
  • Remark 6
  • Proof 7