相關主題
商品描述
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+ specifications
- 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+.
商品描述(中文翻譯)
學習如何在撰寫程式碼之前設計複雜且正確的程式，並解決問題。這本書是一個實用且全面的TLA+程式設計資源，提供豐富且複雜的範例。《實用TLA+》向您展示如何使用TLA+來指定一個複雜系統並測試設計本身的錯誤。
您將學習到即使是一個簡短的TLA+規範也能找到關鍵性的錯誤。首先，通過一個銀行轉帳系統中使用TLA+的範例，讓您了解它如何幫助您設計、測試和建立更好的應用程式。然後，瞭解一些TLA+運算子、邏輯、函數、PlusCal、模型和並發的基礎知識。在此過程中，您將發現如何組織您的藍圖以及如何指定分散式系統和最終一致性。
最後，您將通過一些實際案例應用將所學知識付諸實踐，將TLA+應用於各種實際問題：從算法性能和數據結構到業務代碼和MapReduce。閱讀並使用本書後，您將擁有開始使用TLA+並在重要任務應用中使用它所需的知識。
您將學到什麼：
- 閱讀和撰寫TLA+規範
- 檢查規範中的破壞不變量、競爭條件和活性錯誤
- 設計並發和分散式系統
- 瞭解TLA+如何幫助您日常的生產工作
本書適合對設計和TLA+新手的有編程經驗的讀者。
