عنوان

Practical TLA+ :

(Number (ISBN

148423829X

(Number (ISBN

1484238303

(Number (ISBN

9781484238295

(Number (ISBN

9781484238301

Erroneous ISBN

1484238281

Erroneous ISBN

9781484238288

Title Proper

Practical TLA+ :

General Material Designation

[Book]

Other Title Information

planning driven development /

First Statement of Responsibility

Hillel Wayne.

Place of Publication, Distribution, etc.

[New York, NY] :

Name of Publisher, Distributor, etc.

Apress,

Date of Publication, Distribution, etc.

[2018]

Specific Material Designation and Extent of Item

1 online resource

Text of Note

Includes index.

Text of Note

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.

Text of Note

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.

Text of Note

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.

Text of Note

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

Text of Note

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+.

Source for Acquisition/Subscription Address

Springer Nature

Stock Number

com.springer.onix.9781484238295

International Standard Book Number

9781484238288

International Standard Book Number

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

Number

Edition

Class number

Wayne, Hillel

Date of Transaction

20200823032333.0

Cataloguing Rules (Descriptive Conventions))

pn

Electronic name

[Book]

Y