000			a
999			_c33339 _d33339
008			241118b xxu||||| |||| 00| 0 eng d
020			_a9781484248324
082			_a005.13 _bWAY
100			_aWayne, Hillel
245			_aPractical TLA+ : planning driven development
260			_bApress, _c2018 _aNew York :
300			_axxiii, 221 p. ; _bill., _c26 cm.
365			_b924.00 _c₹ _d01
504			_aIncludes index.
520			_aLearn 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 Learn Read and write TLA+ specs Check specs for broken invariants, race conditions, and liveness bugs Design concurrency and distributed systems Learn how TLA+ can help you with your day-to-day production work Who This Book Is For Those with programming experience who are new to design and to TLA+.
650			_aSoftware development
650			_aScripting languages
650			_aData processing
650			_aActiveWorkers
650			_aBinary search
650			_aDekker's Algorithm
650			_aEnd process
650			_aEXTENDS Integers
650			_aFair process
650			_aMapReduce
650			_aModel checking
650			_aPlusCal
650			_aSymmetry sets
650			_aTemporal Logic
942			_2ddc _cBK