Cantitate/Preț
Produs

Practical TLA+

Autor Hillel Wayne
en Limba Engleză Paperback – 12 oct 2018

Remarcăm în Practical TLA+ o structură progresivă: de la concept la implementare, concepută special pentru a demistifica metodele formale în dezvoltarea software-ului modern. Abordarea diferă de Specifying Systems de Leslie Lamport prin faptul că este mai puțin abstractă și mult mai aplicabilă; în timp ce lucrarea lui Lamport servește ca referință teoretică fundamentală, Hillel Wayne se concentrează pe fluxul de lucru zilnic al unui inginer software. Apreciem modul în care autorul ghidează cititorul prin sintaxa TLA+ și PlusCal folosind exemple tangibile, precum un sistem de transfer bancar, demonstrând rapid cum specificațiile formale pot preveni erori costisitoare de logică. Prima parte a volumului pune bazele teoretice necesare, explorând operatorii, logica temporală și concurența. Cuprinsul indică o tranziție logică spre partea a doua, unde accentul cade pe aplicabilitate. Analizăm studii de caz complexe, de la algoritmi și structuri de date până la sisteme distribuite și modelul MapReduce. Spre deosebire de An Introduction to Practical Formal Methods Using Temporal Logic, care păstrează un ton academic pronunțat, această lucrare publicată de Apress prioritizează rezolvarea problemelor de producție. Reținem că volumul nu cere cunoștințe matematice avansate, oferind în schimb instrumentele practice pentru a verifica invarianții și consistența eventuală a sistemelor complexe. Este o resursă esențială pentru cei care doresc să implementeze „Planning Driven Development” și să elimine bug-urile de design înainte ca prima linie de cod să fie scrisă.

Citește tot Restrânge

Preț: 20990 lei

Preț vechi: 26238 lei
-20%

Puncte Express: 315

Carte disponibilă

Livrare economică 27 mai-10 iunie


Specificații

ISBN-13: 9781484238288
ISBN-10: 1484238281
Pagini: 248
Ilustrații: XXIII, 221 p. 22 illus.
Dimensiuni: 178 x 254 x 14 mm
Greutate: 0.47 kg
Ediția:First Edition
Editura: Apress
Locul publicării:Berkeley, CA, United States

De ce să citești această carte

Recomandăm această carte programatorilor care lucrează cu sisteme distribuite sau concurente și doresc să evite erorile de design subtile. Veți câștiga o metodă riguroasă de a vă testa arhitectura software folosind TLA+, transformând specificațiile abstracte în instrumente practice de verificare. Este un ghid esențial pentru a trece de la scrierea intuitivă de cod la un design software bazat pe dovezi și logică.


Despre autor

Hillel Wayne este un consultant și educator recunoscut în domeniul metodelor formale, specializat în aplicarea acestora în ingineria software industrială. Prin munca sa, Wayne a devenit una dintre vocile principale care promovează utilizarea TLA+ în rândul programatorilor, reușind să traducă concepte matematice complexe în strategii de dezvoltare accesibile. Expertiza sa se concentrează pe îmbunătățirea fiabilității sistemelor software prin design riguros, fiind un promotor activ al instrumentelor care ajută la detectarea erorilor logice înainte de implementare.


Descriere scurtă

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


Cuprins

Part I: The Semantics of TLA+ and PlusCal.- 1. An Example.- 2. PlusCal.- 3. Operators and Functions.- 4. Constants, Models, and Imports.- 5. Concurrency.- 6. Temporal Logic.- Part II: Applying TLA+.- 7. Algorithms.- 8. Data Structures.- 9. State Machines.- 10. Ambiguity and Feature Interation.- 11. Case Study: MapReduce.- Appendix A: Mathematics.- Appendix B: PT library.- Appendix C: PlusCal to TLA+.


Notă biografică

Hillel Wayne is a software consultant who specializes in formal methods and specification. He also writes on empirical engineering, software history, and education. In his free time, he juggles and makes chocolate. He lives in Chicago. You can find his other work at hillelwayne.com or on Twitter at @hillelogram.

Caracteristici

Use TLA+ to uncover complex bugs before you code Practical, useful examples in distributed systems, threading, business logic, and more Three case studies that teach the real-world experience