Specifying SystemsLast modified 29 October 2017
The book Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers has been published by Addison-Wesley Professional, a division of Pearson Education. Click here to order it from the publisher. You can also download a copy for your own use, as well as accompanying material. Please address all comments and suggestions to Leslie Lamport.
The BookThe book is 364 pages long (including a 17-page index). However, most people will want to read only the first part, which comprises the first seven chapters and is 83 pages long. Here is the list of chapters.
The List of CorrectionsThis is a list of all known errors and omissions in the book. If you are the first to report an error, you will be acknowledged in any new edition.
Accompanying MaterialAlso available for downloading is material to accompany the book. This includes the ASCII versions of all specifications from the book, additional modules and configuration files for using the TLC model checker to check some of the specifications, and a few exercises. I hope that readers will provide additional exercises. I would also like to include example specifications written by others. Now, the only other example is the Wildfire challenge problem. The specification of the Alpha memory that it contains will be of particular interest to readers of the memory specifications in Chapter 11. Please contact me if you have any suggestions.
The material is organized hierarchically, with the material for each chapter in a separate folder (directory). Each folder, including the root, has a README file containing the exercises and an explanation of what else is in the directory. The material is available as a Zip file for Windows users and as a gzipped tar file for Unix users.