相關主題
商品描述
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+ 程式設計，並提供豐富且複雜的範例。《Practical TLA+》將教您如何使用 TLA+ 來指定複雜系統並測試設計本身以找出錯誤。
您將學習到，即使是簡短的 TLA+ 規範也能發現關鍵的錯誤。首先，通過一個在銀行轉帳系統中使用 TLA+ 的範例來入門，看看它如何幫助您設計、測試和構建更好的應用程式。接著，了解 TLA+ 的運算子、邏輯、函數、PlusCal、模型和併發的基本知識。在這個過程中，您將發現如何組織您的藍圖，以及如何指定分散式系統和最終一致性。
最後，您將把所學應用於一些實作案例研究應用程式，將 TLA+ 應用於各種實際問題：從演算法性能和資料結構到商業程式碼和 MapReduce。在閱讀並使用本書後，您將具備開始使用 TLA+ 的所需知識，以及如何在您的關鍵任務應用程式中使用它。
您將學到的內容：
- 閱讀和撰寫 TLA+ 規範
- 檢查規範中的不變式破壞、競爭條件和活性錯誤
- 設計併發和分散式系統
- 瞭解 TLA+ 如何幫助您進行日常生產工作
本書適合對象：
有程式設計經驗但對設計和 TLA+ 新手的讀者。
