Specifying Systems

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