| |
| |
List of Figures and Tables | |
| |
| |
Acknowledgments | |
| |
| |
Introduction | |
| |
| |
| |
Getting Started | |
| |
| |
| |
A Little Simple Math | |
| |
| |
| |
Propositional Logic | |
| |
| |
| |
Sets | |
| |
| |
| |
Predicate Logic | |
| |
| |
| |
Formulas and Language | |
| |
| |
| |
Specifying a Simple Clock | |
| |
| |
| |
Behaviors | |
| |
| |
| |
An Hour Clock | |
| |
| |
| |
A Closer Look at the Specification | |
| |
| |
| |
The Specification in TLA+ | |
| |
| |
| |
An Alternative Specification | |
| |
| |
| |
An Asynchronous Interface | |
| |
| |
| |
The First Specification | |
| |
| |
| |
Another Specification | |
| |
| |
| |
Types: A Reminder | |
| |
| |
| |
Definitions | |
| |
| |
| |
Comments | |
| |
| |
| |
A Fifo | |
| |
| |
| |
The Inner Specification | |
| |
| |
| |
Instantiation Examined | |
| |
| |
| |
Instantiation Is Substitution | |
| |
| |
| |
Parametrized Instantiation | |
| |
| |
| |
Implicit Substitutions | |
| |
| |
| |
Instantiation Without Renaming | |
| |
| |
| |
Hiding the Queue | |
| |
| |
| |
A Bounded FIFO | |
| |
| |
| |
What We're Specifying | |
| |
| |
| |
A Caching Memory | |
| |
| |
| |
The Memory Interface | |
| |
| |
| |
Functions | |
| |
| |
| |
A Linearizable Memory | |
| |
| |
| |
Tuples as Functions | |
| |
| |
| |
Recursive Function Definitions | |
| |
| |
| |
A Write-Through Cache | |
| |
| |
| |
Invariance | |
| |
| |
| |
Proving Implementation | |
| |
| |
| |
Some More Math | |
| |
| |
| |
Sets | |
| |
| |
| |
Silly Expressions | |
| |
| |
| |
Recursion Revisited | |
| |
| |
| |
Functions versus Operators | |
| |
| |
| |
Using Functions | |
| |
| |
| |
Choose | |
| |
| |
| |
Writing a Specification: Some Advice | |
| |
| |
| |
Why Specify | |
| |
| |
| |
What to Specify | |
| |
| |
| |
The Grain of Atomicity | |
| |
| |
| |
The Data Structures | |
| |
| |
| |
Writing the Specification | |
| |
| |
| |
Some Further Hints | |
| |
| |
| |
When and How to Specify | |
| |
| |
| |
More Advanced Topics | |
| |
| |
| |
Liveness and Fairness | |
| |
| |
| |
Temporal Formulas | |
| |
| |
| |
Temporal Tautologies | |
| |
| |
| |
Temporal Proof Rules | |
| |
| |
| |
Weak Fairness | |
| |
| |
| |
The Memory Specification | |
| |
| |
| |
The Liveness Requirement | |
| |
| |
| |
Another Way to Write It | |
| |
| |
| |
A Generalization | |
| |
| |
| |
Strong Fairness | |
| |
| |
| |
The Write-Through Cache | |
| |
| |
| |
Quantification | |
| |
| |
| |
Temporal Logic Examined | |
| |
| |
| |
A Review | |
| |
| |
| |
Machine Closure | |
| |
| |
| |
Machine Closure and Possibility | |
| |
| |
| |
Refinement Mappings and Fairness | |
| |
| |
| |
The Unimportance of Liveness | |
| |
| |
| |
Temporal Logic Considered Confusing | |
| |
| |
| |
Real Time | |
| |
| |
| |
The Hour Clock Revisited | |
| |
| |
| |
Real-Time Specifications in General | |
| |
| |
| |
A Real-Time Caching Memory | |
| |
| |
| |
Zeno Specifications | |
| |
| |
| |
Hybrid System Specifications | |
| |
| |
| |
Remarks on Real Time | |
| |
| |
| |
Composing Specifications | |
| |
| |
| |
Composing Two Specifications | |
| |
| |
| |
Composing Many Specifications | |
| |
| |
| |
The FIFO | |
| |
| |
| |
Composition with Shared State | |
| |
| |
| |
Explicit State Changes | |
| |
| |
| |
Composition with Joint Actions | |
| |
| |
| |
A Brief Review | |
| |
| |
| |
A Taxonomy of Composition | |
| |
| |
| |
Interleaving Reconsidered | |
| |
| |
| |
Joint Actions Reconsidered | |
| |
| |
| |
Liveness and Hiding | |
| |
| |
| |
Liveness and Machine Closure | |
| |
| |
| |
Hiding | |
| |
| |
| |
Open-System Specifications | |
| |
| |
| |
Interface Refinement | |
| |
| |
| |
A Binary Hour Clock | |
| |
| |
| |
Refining a Channel | |
| |
| |
| |
Interface Refinement in General | |
| |
| |
| |
Open-System Specifications | |
| |
| |
| |
Should You Compose? | |
| |
| |
| |
Advanced Examples | |
| |
| |
| |
Specifying Data Structures | |
| |
| |
| |
Local Definitions | |
| |
| |
| |
Graphs | |
| |
| |
| |
Solving Differential Equations | |
| |
| |
| |
BNF Grammars | |
| |
| |
| |
Other Memory Specifications | |
| |
| |
| |
The Interface | |
| |
| |
| |
The Correctness Condition | |
| |
| |
| |
A Serial Memory | |
| |
| |
| |
A Sequentially Consistent Memory | |
| |
| |
| |
The Memory Specifications Considered | |
| |
| |
| |
The Tools | |
| |
| |
| |
The Syntactic Analyzer | |
| |
| |
| |
The TLATEX Typesetter | |
| |
| |
| |
Introduction | |
| |
| |
| |
Comment Shading | |
| |
| |
| |
How It Typesets the Specification | |
| |
| |
| |
How It Typesets Comments | |
| |
| |
| |
Adjusting the Output Format | |
| |
| |
| |
Output Files | |
| |
| |
| |
Trouble-Shooting | |
| |
| |
| |
Using LATEX Commands | |
| |
| |
| |
The TLC Model Checker | |
| |
| |
| |
Introduction to TLC | |
| |
| |
| |
What TLC Can Cope With | |
| |
| |
| |
TLC Values | |
| |
| |
| |
How TLC Evaluates Expressions | |
| |
| |
| |
Assignment and Replacement | |
| |
| |
| |
Evaluating Temporal Formulas | |
| |
| |
| |
Overriding Modules | |
| |
| |
| |
How TLC Computes States | |
| |
| |
| |
How TLC Checks Properties | |
| |
| |
| |
Model-Checking Mode | |
| |
| |
| |
Simulation Mode | |
| |
| |
| |
Views and Fingerprints | |
| |
| |
| |
Taking Advantage of Symmetry | |
| |
| |
| |
Limitations of Liveness Checking | |
| |
| |
| |
The TLC Module | |
| |
| |
| |
How to Use TLC | |
| |
| |
| |
Running TLC | |
| |
| |
| |
Debugging a Specification | |
| |
| |
| |
Hints on Using TLC Effectively | |
| |
| |
| |
What TLC Doesn't Do | |
| |
| |
| |
The Fine Print | |
| |
| |
| |
The Grammar of the Configuration File | |
| |
| |
| |
Comparable TLC Values | |
| |
| |
| |
The TLA[superscript +] Language | |
| |
| |
Mini-Manual | |
| |
| |
| |
The Syntax of TLA[superscript +] | |
| |
| |
| |
The Simple Grammar | |
| |
| |
| |
The Complete Grammar | |
| |
| |
| |
Precedence and Associativity | |
| |
| |
| |
Alignment | |
| |
| |
| |
Comments | |
| |
| |
| |
Temporal Formulas | |
| |
| |
| |
Two Anomalies | |
| |
| |
| |
The Lexemes of TLA[superscript +] | |
| |
| |
| |
The Operators of TLA[superscript +] | |
| |
| |
| |
Constant Operators | |
| |
| |
| |
Boolean Operators | |
| |
| |
| |
The Choose Operator | |
| |
| |
| |
Interpretations of Boolean Operators | |
| |
| |
| |
Conditional Constructs | |
| |
| |
| |
The Let/In Construct | |
| |
| |
| |
The Operators of Set Theory | |
| |
| |
| |
Functions | |
| |
| |
| |
Records | |
| |
| |
| |
Tuples | |
| |
| |
| |
Strings | |
| |
| |
| |
Numbers | |
| |
| |
| |
Nonconstant Operators | |
| |
| |
| |
Basic Constant Expressions | |
| |
| |
| |
The Meaning of a State Function | |
| |
| |
| |
Action Operators | |
| |
| |
| |
Temporal Operators | |
| |
| |
| |
The Meaning of a Module | |
| |
| |
| |
Operators and Expressions | |
| |
| |
| |
The Arity and Order of an Operator | |
| |
| |
| |
[lambda] Expressions | |
| |
| |
| |
Simplifying Operator Application | |
| |
| |
| |
Expressions | |
| |
| |
| |
Levels | |
| |
| |
| |
Contexts | |
| |
| |
| |
The Meaning of a [lambda] Expression | |
| |
| |
| |
The Meaning of a Module | |
| |
| |
| |
Extends | |
| |
| |
| |
Declarations | |
| |
| |
| |
Operator Definitions | |
| |
| |
| |
Function Definitions | |
| |
| |
| |
Instantiation | |
| |
| |
| |
Theorems and Assumptions | |
| |
| |
| |
Submodules | |
| |
| |
| |
Correctness of a Module | |
| |
| |
| |
Finding Modules | |
| |
| |
| |
The Semanties of Instantiation | |
| |
| |
| |
The Standard Modules | |
| |
| |
| |
Module Sequences | |
| |
| |
| |
Module FiniteSets | |
| |
| |
| |
Module Bags | |
| |
| |
| |
The Numbers Modules | |