Errata

Here is a list of typos, errors, and other clarifications that were discovered after publication.

Have something else to report? Please email errata.

Thanks for your careful reading!

In the text

• Section 1.6.0, p.21. “storing its out-parameter” -> “storing its out-parameters”
• Section 2.0, p.27. “ssay” -> “say”
• Section 2.0, p.28. “the method implemented” -> “the method is implemented”
• Section 2.1, p.28. “the the” -> “the”
• Chapter 2 Notes, p.62. “and and” -> “and”
• Section 3.3.2, p.76. “proper prefix of 40-n, hours” -> “proper prefix of 40-n, h”
• Section 3.3.3, p.78. “values of the second component” -> “value of the second component”
• Exercise 4.0, p.85. “case Yellow” -> “case YellowLeaf”
• Chapter 4, Notes, p.94. “emphasized is” -> “emphasized in”
• Section 5.8.1, p.125. “It particular” -> “In particular”
• Section 6.6, p.149. The “alternative of rewriting Snoc in terms of Append” is referring to Exercise 6.2.
• Exercise 6.8, p.143. “the liberal version return” -> “the liberal version returns”
• Section 6.4, p.. “we might be access” -> “we might access”
• Section 7.2, p.166. “give an inductive proof for the property that Suc distributes over the first argument to Add” -> “… second argument to Add”
• Section 12.3.2, p.270. Four occurrences of SumpUp should read SumUp.
• Index, p.471. “Müller, Peter” is incorrectly alphabetized at the beginning of the entries for “M”.

In programs

There have also been some changes in the Dafny language and tools since the book’s publication:

• Section 13.3, method Min.

  The first attempt at specifying and implementing Min (Section 13.3.0) does not always assign to out-parameter m. Under Dafny’s previous relaxed definite-assignment rules, this program is allowed and lives up to its specifications. This is the behavior you will get from the legacy command-line interface (CLI), and you can also get it from the new CLI and from Dafny IDE in VS Code if you use the --relax-definite-assignment option. However, starting in Dafny 4.0, the default in the new CLI and IDE is Dafny’s strict definite-assignment mode. It will not accept a method with unassigned out-parameters, even if (as in the case of Min) the compiler can provide a type-safe initialization automatically.

  This means that the specification omission discussed in Section 13.3.1 will actually be detected by Dafny in the Section 13.3.0 program. Once you add the ensures exists ... postcondition from Section 13.3.1, you’ll be able to complete the full program.

  Two more notes about the change in definite-assignment rules: One is that what Dafny does in the relaxed mode is still correct, because the compiler will auto-initialize the value of the out-parameter. The other is that, if you really want the specification from Section 13.3.0, then the implementation given there can be made correct in the strict definite-assignment mode if you add the assignment m := *; at the beginning of the method body.

• Section 13.7, method DetermineElection.

  Since the time the book went into production, some necessary changes were made to the verifier. It now takes more effort to convince the verifier that DetermineElection returns NoWinner under the right circumstances. For more information and two solutions, see the code that accompanies the book on this web site.