Description 
1 online resource 
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 

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; SingleProcess 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 

Chapter 3: Operators and FunctionsOperators; Invariants; Logical Operators; \A and \E; => and ; Expressions; LETIN; IFTHENELSE; 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 
Summary 
Learn how to design complex, correct programs and fix problems before writing a single line of code. This book is a practical, comprehensive resource on TLA+ programming with rich, complex examples. Practical TLA+ shows you how to use TLA+ to specify a complex system and test the design itself for bugs. You'll learn how even a short TLA+ spec can find critical bugs. Start by getting your feet wet with an example of TLA+ used in a bank transfer system, to see how it helps you design, test, and build a better application. Then, get some fundamentals of TLA+ operators, logic, functions, PlusCal, models, and concurrency. Along the way you will discover how to organize your blueprints and how to specify distributed systems and eventual consistency. Finally, you'll put what you learn into practice with some working case study applications, applying TLA+ to a wide variety of practical problems: from algorithm performance and data structures to business code and MapReduce. After reading and using this book, you'll have what you need to get started with TLA+ and how to use it in your missioncritical applications. What You'll LearnRead and write TLA+ specificationsCheck specs for broken invariants, race conditions, and liveness bugsDesign concurrency and distributed systemsLearn how TLA+ can help you with your daytoday production workWho This Book Is ForThose with programming experience who are new to design and to TLA+ 
Notes 
Includes index 

Online resource; title from PDF title page (EBSCO, viewed October 16, 2018) 
Subject 
Programming languages (Electronic computers)


SDL (Computer program language)

Form 
Electronic book

ISBN 
148423829X (electronic bk.) 

1484238303 

9781484238295 (electronic bk.) 

9781484238301 (print) 
