🧠 این کتاب حاصل بیش از ۲۵ سال تجربه و دانش یکی از شناخته‌شده‌ترین دانشمندهای کامپیوتر دنیاست. Specification یعنی یک توضیح دقیق و مکتوب از اینکه یک سیستم قرار است چه کاری انجام بده؛ همراه با روشی برای بررسی اینکه آیا سیستم واقعاً همان‌طور که انتظار داریم کار میکنه یا نه. وقتی برای یک سیستم Specification مینویسیم، در واقع قبل از ساختن آن، تلاش میکنیم بهتر بفهمیمش. چون منطقیه قبل از پیاده‌سازی یک سیستم، اول مطمئن بشیم دقیقاً میدونیم آن سیستم باید چه رفتاری داشته باشه.

🧮 مؤثرترین ابزار برای توصیف یک Specification، Temporal Logic of Actions یا TLA است؛ چون یک پایه ریاضی، یعنی دقیق، برای توصیف سیستم‌ها فراهم میکنه. TLA+ زبانیه که نویسنده برای نوشتن Specificationهای ریاضی توسعه داده. TLA+ به‌صورت رایگان روی وب در دسترسه و هم برای نرم‌افزار و هم برای سخت‌افزار قابل استفاده است. در واقع، Intel با موفقیت زیاد از TLA+ در طراحی یک چیپ جدید استفاده میکنه.

📚 کتاب به چهار بخش تقسیم شده. بخش اول شامل تمام چیزیه که بیشتر برنامه‌نویس‌ها و مهندس‌ها برای نوشتن Specification لازم دارن بدونن. بخش دوم مطالب پیشرفته‌تری برای خواننده‌های حرفه‌ای‌تر داره. بخش‌های سوم و چهارم هم یک Reference Manual برای TLA+ هستن؛ هم خود زبان و هم ابزارهای آن.

💬 نظر

💭 «TLA+ تنها متدولوژی مؤثریه که دیده‌ام و میتونه پیچیدگی الگوریتمی رو به شکلی برای مهندس‌ها قابل‌معنا، قابل‌تصویرسازی و قابل‌اندازه‌گیری کنه.»

—برنن بتسون، Processor Architect در Intel Corporation

📘 این کتابِ مدت‌ها موردانتظار، نشون میده چطور Specificationهای بدون ابهام برای سیستم‌های کامپیوتری پیچیده بنویسی.

🧩 بخش اول یک مقدمه جمع‌وجور و روشن درباره Specification ارائه میده و توضیح میده چطور با دقت ریاضی، ویژگی‌های رفتاری یک سیستم رو توصیف کنیم؛ یعنی اینکه آن سیستم مجاز است چه کارهایی انجام بده. تمرکز اصلی این بخش روی Safety Propertyهاست.

⚙️ بخش دوم کتاب موضوع‌های پیشرفته‌تری رو پوشش میده؛ از جمله Liveness و Fairness، ویژگی‌های Real-Time و Composition.

🛠️ دو بخش پایانی کتاب یک Reference Manual کامل برای زبان و ابزارهای TLA+ ارائه میدن، به‌علاوه یک Mini-Manual کاربردی. TLA+ زبانیه که نویسنده برای نوشتن Specificationهای ساده و شیک از الگوریتم‌ها و پروتکل‌ها و برای Verify کردن درستی طراحی توسعه داده. این زبان همین حالا هم ثابت کرده که برای فهم و ساخت سیستم‌های Concurrent و Distributed کمک بسیار ارزشمندیه. ابزارهای تحلیل Syntax و Model Checking برای TLA+ به‌صورت رایگان از وب در دسترسن، و آنجا میتونی مطالب تکمیلی این کتاب، از جمله تمرین‌ها، رو هم پیدا کنی.

📖 فهرست مطالب

بخش ۱. شروع کار

فصل ۱. کمی ریاضی ساده

فصل ۲. Specification یک ساعت ساده

فصل ۳. یک Interface ناهمگام

فصل ۴. یک FIFO

فصل ۵. یک حافظه Caching

فصل ۶. کمی ریاضی بیشتر

فصل ۷. نوشتن Specification: چند توصیه

بخش ۲. موضوع‌های پیشرفته‌تر

فصل ۸. Liveness و Fairness

فصل ۹. Real Time

فصل ۱۰. ترکیب کردن Specificationها

فصل ۱۱. مثال‌های پیشرفته

بخش ۳. ابزارها

فصل ۱۲. Syntactic Analyzer

فصل ۱۳. Typesetter مربوط به TLATEX

فصل ۱۴. TLC Model Checker

بخش ۴. زبان TLA+

فصل ۱۵. Syntax زبان TLA+

فصل ۱۶. Operatorهای TLA+

فصل ۱۷. معنای یک Module

فصل ۱۸. Moduleهای استاندارد

👤 درباره نویسنده

👨‍🔬 لزلی لمپورت، دانشمند کامپیوتر، به‌خاطر مشارکت‌های مهمش در Concurrent Computing و سیستم‌های Distributed شناخته میشه. مقاله او با عنوان Time, Clocks, and the Ordering of Events in a Distributed System به‌خاطر اثر ماندگارش روی این حوزه مورد تقدیر قرار گرفته.

📚 لمپورت همین‌طور به‌خاطر ساخت سیستم حروف‌چینی LaTeX و کتاب پرفروش LaTeX, Second Edition شناخته میشه؛ کتابی که آن را مستند کرده و در سال ۱۹۹۴ توسط Addison-Wesley منتشر شده. او حالا در Microsoft Research در مانتین ویو، کالیفرنیا فعالیت میکنه و کار روی TLA+ رو در Digital Systems Research Center، که بعدها Compaq شد، در پالو آلتو شروع کرد. لمپورت دکترای ریاضی خودش رو از Brandeis University گرفته و عضو National Academy of Engineering است.

This book is the distillation of over 25 years of work by one of the world's most renowned computer scientists. A specification is a written description of what a system is supposed to do, plus a way of checking to make sure that it works. Specifying a system helps us understand it. It's a good idea to understand a system before building it, so it's a good idea to write a specification of a system before implementing it. The most effective tool to describe a specification is the Temporal Logic of Actions, or TLA, because it provides a mathematical, i.e. precise, foundation for describing systems. TLA+ is the language the author developed to write the mathematical specifications. TLA+ is available freely on the web. It can be used for both software and hardware. In fact, Intel is using TLA+ with great success in the design of a new chip. The book is divided into four parts. The first part contains all that most programmers and engineers need to know about writing specifications. The second part contains more advanced material for more sophisticated readers. The third and fourth parts comprise a reference manual for TLA+ - both the language itself as well as its tools.

"TLA+ represents the only effective methodology I've seen for visualizing and quantifying algorithmic complexity in a way that is meaningful to engineers."

--Brannon Batson, Processor Architect, Intel Corporation

This long-awaited book shows how to write unambiguous specifications of complex computer systems.

The first part provides a concise and lucid introduction to specification, explaining how to describe, with mathematical precision, the behavioral properties of a system--what that system is allowed to do. The emphasis here is on safety properties.

The second part of the book covers more advanced topics, including liveness and fairness, real-time properties, and composition.

The book's final two parts provide a complete reference manual for the TLA+ language and tools, as well as a handy mini-manual. TLA+ is the language developed by the author for writing simple and elegant specifications of algorithms and protocols and for verifying the correctness of a design. The language already has proved to be a valuable aid in understanding and building concurrent and distributed systems. Tools for TLA+ syntax analysis and model checking are freely available from the Web, where you can also find supplemental materials for this book, including exercises.

Table of Contents

Part I. Getting Started

Chapter 1. A Little Simple Math

Chapter 2. Specifying a Simple Clock

Chapter 3. An Asynchronous Interface

Chapter 4. A FIFO

Chapter 5. A Caching Memory

Chapter 6. Some More Math

Chapter 7. Writing a Specification: Some Advice

Part II. More Advanced Topics

Chapter 8. Liveness and Fairness

Chapter 9. Real Time

Chapter 10. Composing Specifications

Chapter 11. Advanced Examples

Part III. The Tools

Chapter 12. The Syntactic Analyzer

Chapter 13. The TLATEX Typesetter

Chapter 14. The TLC Model Checker

Part IV. The TLA+ Language

Chapter 15. The Syntax of TLA+

Chapter 16. The Operators of TLA+

Chapter 17. The Meaning of a Module

Chapter 18. The Standard Modules

About the Author

Leslie Lamport, a computer scientist, is well known for his contributions to concurrent computing and distributed systems. His "Time, Clocks, and the Ordering of Events in a Distributed System" paper has been honored for its enduring influence on the field. Lamport is also known for creating the LaTeX typesetting system and the best-selling book, LaTeX, Second Edition, which documents it (Addison-Wesley, 1994). Now at Microsoft Research in Mountain View, California, he began his work on TLA+ at the Digital (later Compaq) Systems Research Center in Palo Alto. Lamport, who earned his Ph.D. in mathematics from Brandeis University, is a member of the National Academy of Engineering.