Part I: The Semantics of TLA+ and PlusCal1. An Example2.
PlusCal3. Operators and Functions4. Constants, Models, and
Imports5. Concurrency6. Temporal LogicPart II: Applying
7. Algorithms8. Data Structures9. State Machines10. Ambiguity and Feature Interation11. Case Study: MapReduceAppendix A: MathematicsAppendix B: PT libraryAppendix C: PlusCal to TLA+
Hillel Wayne is a software consultant who specializes in formal methods and specification. He also writes on empirical engineering, software history, and education. In his free time, he juggles and makes chocolate. He lives in Chicago. You can find his other work at hillelwayne.com or on Twitter at @hillelogram.