PaperlayerView exact revision on arXiv

Source-linked AI summary

How to Verify a Turing Machine with Dafny

Edgar F. A. Lederer

arXiv:2601.15230v1cs.LO

TL;DR

Teaching Turing machines can be fragile, while their explanations may rely on informal descriptions and sample executions. This paper verifies two such machines using Dafny and concludes that the verifier is suitable for the task.

  • Problem

    Whether teaching Turing machines behave as intended is not trivial, and their functioning may be explained through prose and sample executions.

    Source: §1 · p. 1, §6 · p. 49

  • Method

    The paper uses Dafny to verify a machine for nested parentheses and a textbook machine deciding whether a unary word’s length is a power of two.

    Source: §1 · p. 2

  • Results

    Both machines are verified, and the author concludes that Dafny is suitable for their verification.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The proof’s technical details and repeated checks are described as impractical to handle reliably without a machine and a tool such as Dafny.

    Source: §6 · p. 49

    The author suggests that verifying monolithic machines more complex than the two studied may be infeasible.

    Source: §5 · p. 45

Abstract

from arXiv · show

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.

1 Introduction

Teaching Turing machines can be fragile, making it nontrivial to know whether they behave as intended. The paper formally verifies two such machines with Dafny and concludes that Dafny is suitable for the task.

1 Introduction

  • The author describes teaching Turing machines as fragile artifacts whose intended behavior is not always easy to establish.The paper frames verification of these machines as a challenging task.Source: §1 · pp. 1–2
  • Testing can uncover design errors, but the author asks whether formal proof can establish correctness rather than merely support belief in it.The author reports testing all inputs up to a chosen length before becoming confident in a machine’s correctness.Source: §1 · p. 1
  • The verification targets are a machine for correctly nested and juxtaposed parentheses and a textbook machine deciding whether a unary word’s length is a power of two.The author reports that techniques developed for the first machine also applied to the second, though its development was more challenging.Source: §1 · p. 2
  • Both machines are verified, and the author concludes that Dafny is suitable for their verification.The paper also aims to demonstrate Dafny’s suitability alongside verifying the machines themselves.Source: §1 · p. 2

2 The Turing Machine Model

The paper adopts Sipser’s Turing-machine model, in which a finite-state control and read-write head operate on a one-sided tape. Computation proceeds through configurations until the machine accepts, rejects, or continues indefinitely.

2 The Turing Machine Model

  • A Turing machine decides whether an input has a property by halting and accepting or rejecting, though it may instead run forever.The machine’s task is to determine whether an input word has the considered property.Source: §2 · pp. 2–3
  • The model uses a finite-state control, a tape extending rightward from a beginning, and a read-write head that reads, overwrites, and moves one square.The head moves left only when it is not at the tape’s beginning.Source: §2 · pp. 2–3
  • A configuration is determined by the control state, tape contents, and head position; accepting and rejecting configurations are halting configurations.Source: §2 · p. 3
  • Computation starts with the input at the beginning of the tape and the head at its beginning, then follows uniquely determined configurations until halting.The start state is qstart, and the input is followed by blank symbols.Source: §2 · p. 3
  • For a continuing configuration, the transition function determines the new state, written symbol, and head direction from the current state and read symbol.Only the symbol under the head changes, and the head moves at most one position; halting states have no successor.Source: §2 · pp. 3–4
  • Although the model’s tape is infinite, only a finite portion can contain non-blank symbols at any point in a computation.A finite tape could be extended with blank squares whenever the machine ran out of space.Source: §2 · p. 4

3 The First Example Machine: Parentheses

The section develops and verifies a Turing-machine decider for correctly nested parentheses, implemented by simulating a deterministic pushdown automaton on a tape. It specifies the decision conditions and proves the machine’s behavior and termination in Dafny using invariants and progress measures, including properties of the tape at termination.

3.1 The Language

  • Membership is specified by equal numbers of left and right parentheses and no prefix containing more right than left parentheses, though their equivalence to the grammar is not formally proven.Source: §3.1 · p. 5
  • A verified test oracle implements the same specification as the Turing machine using simpler code, providing a high-level view for testing the mechanism before verification.Source: §3.1 · p. 6

3.2 The Machine

  • The machine simulates a deterministic pushdown automaton: it pushes for each left parenthesis, pops for each right parenthesis, and rejects when a pop is impossible or stack symbols remain at the end.It accepts when the input is fully scanned without an unmatched right parenthesis and no stack symbols remain, corresponding to equal counts and valid prefixes.Source: §3.1 · p. 6, §3.2 · p. 10
  • To implement stack operations with a sequential tape head, the machine marks each parenthesis with x, travels to the stack area, updates it, then returns and restores the parenthesis.The control state retains whether the marked symbol was a left or right parenthesis.Source: §3.2 · p. 10
  • A tape of length 2n + 1 suffices for an input of length n, and Dafny will prove this bound.The machine may write n stack symbols beyond the input; the extra cell also provides a blank when n = 0.Source: §3.2 · p. 11
  • A single loop dispatches on control state and tape symbol to update the tape, head, and state; left moves are guarded at the tape boundary, and a final false assertion marks unhandled transitions as unreachable.The boundary guard mechanically preserves the rule that the head stays put when a left move would cross the tape start.Source: §3.2 · p. 13

3.3 Verification

  • The proof combines control-state-specific local invariants with state-independent global conditions, describing tape contents and tracking the head position, investigated-parenthesis count, and stack size.The tape contains the transformed input, optionally one marking symbol, then stack symbols and blank cells.Source: §3.3 · pp. 14–16
  • Dafny verifies the left-minus-right invariant and absence of runtime errors, but the related proof obligations appear too intertwined for a more modular proof.The proof also establishes that the final false assertion is unreachable.Source: §3.3 · pp. 15, 20
  • In states q1 and q2, the invariant a[k] = LP lets the proof show that replacing the sole marking symbol with a left parenthesis restores the transformed input on the tape.The machine first marks the parenthesis, later finds that mark, and restores its original symbol.Source: §3.3 · pp. 17–18
  • The left-minus-right invariant equates the difference in parentheses seen on the tape with that in the corresponding input prefix.Ghost counters track the parentheses seen and their difference, linking these quantities to the stack symbols and processed input.Source: §3.3 · pp. 18–20
  • The never-more invariant states that each input prefix has at least as many left as right parentheses, and Dafny proves it automatically.The accumulated-invariant lemma offers intuition for the proof, but cannot be applied literally because the machine loop does not match its form.Source: §3.3 · pp. 20–21
  • The proof establishes Δa(k) ≥ 0 as a global invariant and concludes that whenever the machine halts, it yields the correct result.The invariant follows from local invariants for each control state.Source: §3.3 · pp. 22–23
  • At termination, acceptance is equivalent to Θa(a.Length) and Δa(a.Length) = 0; each rejecting state violates at least one of these conditions.The proof checks the accepting state and both ways of reaching rejection against the global invariants.Source: §3.3 · pp. 22–23
  • Termination follows from a three-part lexicographic measure: remaining input length, control-state order, and head-position distance.The input-length component decreases as parentheses are handled; the state and head-position components account for intermediate transitions and moves within a state.Source: §3.3 · pp. 23–24
  • The added postconditions describe the tape contents at termination and input-length constraints, which Dafny proves automatically from the existing postconditions.Accepted inputs have even length, while rejected inputs have length at least one; these length facts follow from the original postconditions rather than the machine’s mechanics.Source: §3.3 · pp. 24–25

4 The Second Example Machine: Sipser’s M2

This section presents Sipser’s M2, a decider for unary strings whose lengths are powers of two, and formalizes its tape-based computation in Dafny. It develops invariants for the division cycles and proves partial correctness and termination, establishing total correctness against the specification.

4.1 The Language

  • M2 decides the unary language of strings with power-of-two lengths by repeatedly halving an even count and accepting exactly when the resulting odd count is one.Zero is rejected; the supporting lemmas state that one is a power of two and the only odd natural number that is.Source: §4.1 · pp. 25–26

4.2 The Machine

  • The machine uses tape symbols blank, 0, and x, and its state-transition implementation is placed directly in the specified machine rather than separated from it.The transition function assigns the otherwise impossible q0-on-x case to rejection, while the implementation omits that transition and proves it cannot occur.Source: §4.2 · pp. 27, 29
  • Each scan crosses off every second zero to compute a quotient while q1–q3 track the remainder; even counts lead to another halving cycle, while odd counts above one reject.Returning the head to the beginning uses the first tape blank as a marker; that blank still represents the original first zero, not a crossed-off symbol.Source: §4.2 · pp. 28–29

4.3 Verification

  • Dafny verification proceeds through runtime safety, a halving invariant, a power-of-two invariant, partial correctness, and finally termination for total correctness.The authors report that verification succeeds at the end of each of the five steps.Source: §4.3 · p. 30
  • Position and tape-content invariants ensure tape accesses remain in range, and Dafny verifies that the unimplemented q0-on-x transition is unreachable.The tape has length n + 1 for an input of length n; the head may move one position beyond it only after computation stops.Source: §4.2 · p. 29, §4.3 · p. 31
  • Local invariants relate snapshot and tape zero counts during division: the counts are equal in q1, doubled in q2, and one less than doubled in q3.These relations capture the odd/even progress of crossing off every second zero.Source: §4.3 · pp. 33–34
  • Because Dafny treats an array update as changing the whole array, the proof records a snapshot and uses a zero-count lemma to show the update leaves counts before the head unchanged.Dafny proves the lemma automatically, and the resulting assertion is verified.Source: §4.3 · pp. 35–37
  • At entry to the first division cycle, the zero count on the tape and snapshot equals the input length, establishing the power-of-two invariant’s initial condition.The proof uses that the input alphabet contains only zeroes and a lemma counting zeroes in the initialized tape prefix.Source: §4.3 · pp. 38–39
  • The power-of-two invariant is maintained across division cycles, with the q4-to-q1 transition relying on the halving invariant and an evenness lemma.The other transitions between q1 and q4 do not affect this invariant.Source: §4.3 · pp. 39–40
  • On acceptance, the snapshot has one zero, so the power-of-two invariant implies the input length is a power of two; rejection from an empty input establishes that the length is not a power of two.Source: §4.3 · p. 41
  • In qrej, the snapshot has an odd number of zeroes, at least three, so it is not a power of two; invariant I8 then shows a.Length is not a power of two.This completes the proof of partial correctness.Source: §4.3 · p. 42
  • A four-component lexicographic ordering unites high-level progress through snapshots and halving with low-level progress through individual transitions.Its components measure progress made by specified transition classes.Source: §4.3 · p. 43
  • The first component measures the start-state transitions, while the next measures division cycles by the strict decrease in snapshot zeroes when q4 returns to q1.Dafny verifies that the snapshot-count expression strictly decreases and is bounded below by zero.Source: §4.3 · p. 43
  • The remaining components measure progress through completion or the return scan, then through head movement across the tape in q1–q3 and back in q4.Dafny verifies both expressions strictly decrease and are bounded below by zero.Source: §4.3 · p. 44
  • The partition of all transitions across the lexicographic ordering completes the termination proof and establishes total correctness against the specification.Dafny verifies that each component strictly decreases when used and is bounded below by zero.Source: §4.3 · p. 44

5 Related Work

Earlier work formalizes frameworks for constructing and verifying Turing machines, often applying them to universal machines. This paper instead verifies two monolithic teaching machines not designed with verification in mind.

5 Related Work

  • The paper’s examples are fixed, monolithic teaching machines, unlike prior frameworks for systematically constructing machines; verifying more complex monolithic machines may be infeasible.The paper describes its two verifications as a realization of the “nightmare” attributed to proving monolithic machines.Source: §5 · pp. 44–45
  • Asperti and Ricciotti formalize machine composition and relational specifications, then use their framework to construct and verify a universal machine.Their semantics relate initial and final tape contents, omitting the resulting control state; this simplifies sequential composition but complicates conditional and iterative composition.Source: §5 · p. 46
  • Forster, Kunze, and Wuttke build a three-layer Coq framework for multi-tape machines and apply it to a universal machine and a compiler to mono-tape machines.Their framework also supports time and space complexity analysis.Source: §5 · pp. 46–47
  • The paper rewrites Sipser’s M2 in the Forster et al. framework as a 56-state machine, compared with the original’s 7 states.This illustrates the contrast between framework-based construction and verification of an existing monolithic machine.Source: §5 · pp. 44, 47
  • Xu, Zhang, and Urban formalize textbook computability material in Isabelle/HOL, including Turing-machine compilation and the equivalence of three computation models.Their formalization stays close to the textbook’s unusually detailed informal proofs.Source: §5 · pp. 47–48
  • Xu et al. prove correctness of dither and copy using total-correctness Hoare triples and composition rules, with copy built from three proven components.The component proofs use invariants and termination metrics with the same state-dependent structure as those in this paper.Source: §5 · p. 48

6 Conclusions

The paper concludes that verifying Turing machines is a “nightmare,” while Dafny makes the task enjoyable. Its detailed proofs also expose a tension between verification automation and human understanding.

6 Conclusions

  • The author concludes that verifying a Turing machine is a “nightmare,” but using Dafny transforms the task into a pleasure.The author reports that verifying each machine takes a few seconds in both development environments.Source: §6 · pp. 48–49
  • Sipser’s M2 receives less than two pages of explanation and a sample execution in the textbook, but a little over 20 pages of discussion and proof here.The author contrasts intuitive understanding from brief explanations with the technical detail required for formal verification.Source: §6 · p. 49
  • Dafny’s automation can reduce the user’s opportunity to think through the subject, so the author added an explanatory lemma for the “never-more invariant.”The author cautions that such explanations do not indicate what Dafny itself does.Source: §6 · p. 49
  • Developing and repeatedly checking the many lemmas, invariants, and bound functions requires a machine, even for an extremely meticulous worker.The author distinguishes the effort of developing a proof from checking its final form.Source: §6 · p. 49

A.1 The Accumulated Invariant Lemma

The Accumulated Invariant Lemma turns an invariant I(k) into a prefix-wide invariant covering every index from zero through k. Under its stated loop conditions, the accumulated predicate is itself maintained.

A.1 The Accumulated Invariant Lemma

  • I∀(k) asserts I(j) for every j between 0 and k, inclusive.The lemma applies to a loop that initializes k to zero, executes C, then increments k, where C does not modify k.Source: §A.1 · p. 50
  • If I(k) is initially true and maintained by the loop body under guard B, then I∀(k) is also an invariant.The formal condition uses weakest precondition for partial correctness and assumes C does not assign to k.Source: §A.1 · p. 50
  • At loop entry, I(0) implies I∀(0), since the prefix condition reduces to the single case j = 0.The proof uses the definition of I∀ and the one-point rule.Source: §A.1 · p. 51
  • For maintenance, I∀(k+1) splits into I∀(k) and I(k+1), while I∀(k) supplies I(k) for the loop-body step.The proof combines the assumed preservation of I with the loop guard to establish both parts of the next prefix.Source: §A.1 · pp. 51–52
  • The appendix also sketches a Dafny encoding that assumes I(0) and preservation of I, then asks Dafny to prove I_forall as a loop invariant.The proof outline introduces an accumulated-invariant lemma method and a loop with separate I and I_forall invariants.Source: §A.1 · pp. 52–53

A.2 The Remaining Cases for Showing ∆a(k) ≥0 •

The remaining proof cases establish nonnegativity of ∆a(k) by relating local state changes to the tape-derived quantity and using the applicable state condition.

A.2 The Remaining Cases for Showing ∆a(k) ≥0

  • In q3 and q4, s decreases by one as k advances, and a[k] = RP makes that change match the decrease in ∆a(k).The case conditions yield ∆a(k) ≥ 0, using s = 0 for one case and s ≥ 0 for the other.Source: §A.2 · pp. 53–54
  • In q5, s stays constant while k advances and a[k] = RP, so s = ∆a(k+1) implies ∆a(k) ≥ 1.The case assumes s ≥ 0.Source: §A.2 · p. 53
  • In qacc, s and k remain unchanged and s = 0, which gives ∆a(k) = 0.Source: §A.2 · p. 53
  • In qrej via q0, s and k remain unchanged and s ≥ 1, yielding ∆a(k) ≥ 1.Source: §A.2 · p. 54

B.1 Proofs of the Three Lemmas

The lemmas establish basic characterizations of powers of two: 1 is a power of two, even candidates can be halved, and an odd power of two must be 1.

B.1 Proofs of the Three Lemmas

  • For even n, isPowerOf2(n) holds exactly when isPowerOf2(n / 2) holds.The two directions are proved separately and combined in the equivalence.Source: §B.1 · p. 55
  • For odd n, if isPowerOf2(n) holds, then n == 1.The proof uses n == 2 * (n / 2) + 1 to conclude the exponent is zero.Source: §B.1 · pp. 55–56
  • The base case is established by showing that 1 is a power of two.The proof identifies 1 with power(2, 0).Source: §B.1 · p. 56

C Sipser’s M2 in the Formalization with Coq

Sipser’s M2 is adapted to the Coq formalization without changing its structure, with adjustments for tape-end behavior and halting transitions. The resulting one-tape machine has 56 internal states, while its behavior on inputs containing x remains unspecified and its realization is unverified.

C Sipser’s M2 in the Formalization with Coq

  • At the left tape boundary, the machine rewinds until the head overflows and enters q0 because it has not yet seen a zero.The original structure needs no rewrite; the adjustment replaces rewinding to a blank symbol with rewinding to the tape boundary.Source: C Sipser’s M2 in the Formalization… · p. 56
  • Transitions leading to halting states keep the head in place rather than moving it arbitrarily to the right.This is an additional capability of the new machine model.Source: C Sipser’s M2 in the Formalization… · p. 56
  • The Coq-adjusted Sipser’s M2 is represented as a state-transition diagram and a one-tape machine with 56 internal states.The construction comprises nine machines, each realizing interactions among selected states and their outgoing transitions.Source: Figure 8 · p. 57, C Sipser’s M2 in the Formalization… · pp. 57–58
  • The machine’s behavior is unspecified on inputs containing x, and the realization relation has not been verified.Termination and realization were tested by Java simulation on zero-only inputs of lengths 0 through 216.Source: C Sipser’s M2 in the Formalization… · pp. 57–58
Loading 2601.15230v1…