Specifying Systems

Leslie Lamport

Last modified on 16 January 2022
This book won an award for its cover design at the New England Book Show. A production editor at Addison-Wesley wrote:
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 [are] 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.   You can click here to order it from the publisher, or download a copy for your own use. You can also download accompanying material.  

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.  

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