Practical TLA+ : planning driven development /: planning driven development. ([2018])

• Record Type: Book
• Further Information: Note: Hillel Wayne.
• Authors: Wayne, Hillel
• Contents: Intro; Table of Contents; About the Author; About the Technical Reviewer; Acknowledgments; Introduction; Part I: The Semantics of TLA+ and PlusCal; Chapter 1: An Example; The Problem; Boilerplate; Specifying; Implementing; Verifying; Initial Conditions; Multiple Processes; Temporal Properties; Summary; Chapter 2: PlusCal; Introduction; Specifications; Layout of a Spec; Expressions; Values; PlusCal Algorithm Body; Assignment; assert; skip; if; while; Macros; Example; Complex Behaviors; Multiple Starting States; Example; Nondeterministic Behavior; Either; With; Example; Summary Chapter 3: Operators and FunctionsOperators; Invariants; Logical Operators; \A and \E; => and ; Expressions; LET-IN; IF-THEN-ELSE; CASE; CHOOSE; Functions; Functions and Operators; DOMAIN; Outline Placeholder; Outline Placeholder; Sets of Functions; Example; Summary; Chapter 4: Constants, Models, and Imports; Constants; Ordinary Assignment; Model Values; Sets of Model Values; ASSUME; Infinite Sets; TLC Runtime; Configuration; Error Traces; The TLC Module; Print and PrintT; Assert; Permutations and SortSeq; Imports; EXTENDS; INSTANCE; Summary; Chapter 5: Concurrency; Labels; Processes AwaitDeadlocks; Process Sets; Procedures; Example; Summary; Chapter 6: Temporal Logic; Termination; Stuttering; Fairness, Weak and Strong; The Temporal Operators; Outline Placeholder; Outline Placeholder; Outline Placeholder; [ ] and [ ]; Limitations of Liveness; Example; Summary; Part II: Applying TLA+; Chapter 7: Algorithms; Single-Process Algorithms; Max; Leftpad; Properties of Algorithms; Multiprocess Algorithm; Summary; Chapter 8: Data Structures; Validation; Example; Summary; Chapter 9: State Machines; State Machines; Scaffolding Implementations; Ghost Variables; Summary Chapter 10: Business LogicThe Requirements; Adding Invariants; Adding Liveness; Adding Reservations; Updating Assumptions; Expiring Reservations; Summary; Chapter 11: MapReduce; Problem Overview; Part One: Basics; Part Two: Liveness; Part Three: Statuses; Exercise; Summary; Appendix A: Math; Propositional Logic; Evaluating Propositions in TLA+; Sets; Predicate Logic; Evaluating Predicates in TLA+; Appendix B: The PT Module; Appendix C: PlusCal to TLA+; Temporal Logic; Actions; TLA; Limitations of PlusCal; Index
• Publisher Details: New York, NY : Apress
• Publication Date: 2018
• Extent: 1 online resource
• Subjects: 005.13; Computer science; Programming languages (Electronic computers); SDL (Computer program language); COMPUTERS / Programming Languages / General; Computers -- Programming -- General; Computers -- Software Development & Engineering -- General; Computer programming / software development; Software Engineering; Software engineering; Computers -- Programming Languages -- General; Programming & scripting languages: general; Electronic books
• Languages: English
• ISBNs: 9781484238295
• Related ISBNs: 148423829X; 9781484238288
• Notes: Note: Online resource; title from PDF title page (EBSCO, viewed October 16, 2018).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.