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; 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.
متن يادداشت
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.
بدون عنوان
0
بدون عنوان
8
بدون عنوان
8
بدون عنوان
8
یادداشتهای مربوط به خلاصه یا چکیده
متن يادداشت
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 mission-critical 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 day-to-day production workWho This Book Is ForThose with programming experience who are new to design and to TLA+.
یادداشتهای مربوط به سفارشات
منبع سفارش / آدرس اشتراک
Springer Nature
شماره انبار
com.springer.onix.9781484238295
ویراست دیگر از اثر در قالب دیگر رسانه
شماره استاندارد بين المللي کتاب و موسيقي
9781484238288
شماره استاندارد بين المللي کتاب و موسيقي
9781484238301
موضوع (اسم عام یاعبارت اسمی عام)
موضوع مستند نشده
Programming languages (Electronic computers)
موضوع مستند نشده
SDL (Computer program language)
موضوع مستند نشده
Computer programming-- software development.
موضوع مستند نشده
COMPUTERS-- Programming Languages-- General.
موضوع مستند نشده
Programming & scripting languages: general.
موضوع مستند نشده
Programming languages (Electronic computers)
موضوع مستند نشده
SDL (Computer program language)
موضوع مستند نشده
Software Engineering.
مقوله موضوعی
موضوع مستند نشده
COM-- 051010
موضوع مستند نشده
UMC
موضوع مستند نشده
UMX
موضوع مستند نشده
UMX
رده بندی ديویی
شماره
005
.
13
ويراست
23
رده بندی کنگره
شماره رده
QA76
.
7
نام شخص به منزله سر شناسه - (مسئولیت معنوی درجه اول )