Page 71: The explanation for the expression "some address" should read "says that the address book is not empty: there is some pair mapping a name to an address or to a name". The formula "all n: Name | lone n.address" should read "all n: Name | lone n.address & Address".

Page 97: In the explanation of cardinality constraints, "this.e" should be replaced by "this.f" in the following sentence: "When e is an expression denoting a set, it can be prefixed with a multiplicity that bounds the cardinality of this.e".[thanks to Roger Costello]

Page 138: In the code for the boolean module, the signature declaration should read "abstract sig Boolean".

Page 148: The second batch of declarations is missing the declaration "b': Book". [thanks to readers of the Japanese edition]

Page 197: The traces predicate assumes that the scope assigns enough time atoms for all the events; if not, time-traveling events are possible. To prevent this, the traces predicate should include the formula "all e: Event | e.post = e.pre.next". The predicate also admits duplicate events, which are confusing, and can be eliminated by changing the quantification to read "all t: Time | one e: Event { ...". [thanks to Jonathan Eldridge, Ardra Hren, Natalie Klotz, Abigail Moses for the first and Brett Decker, Junsong Li for the second; all students in Tim Nelson's "Logic for Hackers" class at Brown University in Spring 2014]

Page 218: The assertion PasteCut (shown on p.203) should be repeated in the figure on this page. [thanks to readers of the Japanese edition]

Page 227, 229, 230: The paths for all the imported modules referenced in the open statements on page 227, and in figures on pages 229 and 230 should be prefixed "examples". [thanks to readers of the Japanese edition]

Page 230: The quantification in writeOK should include the variable am'.[thanks to readers of the Japanese edition]

Page 242: "Baker Street is followed by Liverpool Street" should read "Liverpool Street is followed by Baker Street".[thanks to readers of the Japanese edition]

Page 239, Exercise A.1.9: The text confuses the variables R and r. Corrected version here. [thanks to Tim Nelson, Spencer Gordon, Cody Mello, and Kenny Micklas]

Page 244, Exercise A.2.2: "In this problem, you are given a model of a simple address book program, with operations to add, delete,viol and look up a name, and an invariant ..." should read "In this problem, you are given a model of a simple address book program, with operations to add, delete and look up a name, and an invariant ...". [thanks to Spencer Gordon]

Page 247, Exercise A.3.1: "Everybody loves my baby". A note for international readers who might be confused by the use of the word "baby" here: in American English (although less often nowadays), the word "baby" is used by a man---in an affectionate but perhaps demeaning way---to refer to a romantic partner. [thanks to Shriram Krishnamurthi]

Page 262: The grammar production for commands should read "cmdDecl ::= [name ":"] ("run"|"check") (name|block) scope" (with all the parentheses except those around the name clause switched from square to round). [thanks to Michael Sperberg-McQueen]

Page 307: In the explanation of the trace, Key0 and Key1 should be exchanged in the mention of issued keys for the second and third state.[thanks to readers of the Japanese edition]

Page 321: In the OCL model, "Desk.allInstances.key4issued->excludes(c.key4snd) " should instead be "Desk.allInstances.key4issued@pre->excludes(c.key4snd)".[thanks to readers of the Japanese edition]