Specifying Systems

Last modified 29 October 2017
This book won an award for its cover design at the New England Book Show. A production editor at Addison-Wesley writes
For those of you who are unfamiliar with the Book Show, I think of it as the Emmys of book production. Many different publishers participate, competition is steep, and there often hundreds of nominations for the judges to review.

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 Book

The 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.
  1. A Little Simple Math
  2. Specifying a Simple Clock
  3. An Asynchronous Interface
  4. A FIFO
  5. A Caching Memory
  6. Some More Math
  7. Writing a Specification: Some Advice
  8. Liveness and Fairness
  9. Real Time
  10. Composing Specifications
  11. Advanced Examples
  12. The Syntactic Analyzer
  13. The TLATeX Typesetter
  14. The TLC Model Checker
  15. The Syntax of TLA+
  16. The Operators of TLA+
  17. The Meaning of a Module
  18. The Standard Modules

The List of Corrections

This 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 Material

Also 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.

Downloading

The Book
The book Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers by Leslie Lamport is copyright (c) 2002 by Pearson Education, Inc.   It may not be reproduced or distributed for commercial purposes, or for any purpose other than for personal use, without the prior written permission of the publisher.
Postscript     Gzipped Postscript     PDF

The List of Corrections
PDF

The Supporting Material
Windows Zip File     Unix  Gzipped Tar File

An alternative pdf version with the table of contents as bookmarks.