简介

翻译自：https://learntla.com/

Note

Welcome to Learn TLA+! This is still a work in progress, please see What’s New for updates and please raise any questions or concerns at the github repo. I’d love to hear your feedback! 欢迎来到学习TLA+！该教程目前还在逐步完善中，访问最近更新页面查看教程更新日志；有任何问题或建议，移步该教程的github仓库提issue。 （对中文翻译有任何改进建议，请联系[email protected]）

(In the meantime, you can find the old version at old.learntla.com.) 老版本：old.learntla.com。

学习TLA+

Most software flaws come from one of two places. A code bug is when the code doesn’t match our design— for example, an off-by-one error, or a null dereference. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, we’re just taught to “think about it really hard”. 大多数软件缺陷，是由两个原因之一造成的。其一是编码错误，即代码与设计不符：如off-by-one错误或解引用空指针。如今有很多手段辅助我们发现编码错误（静态分析等）。另一个就是设计缺陷了。然而，面对设计缺陷，我们常常只能做到“使劲想想”。

TLA+ is a “formal specification language”, a means of designing systems that lets you directly test those designs. Developed by the Turing award-winner Leslie Lamport, TLA+ has been endorsed by companies like AWS, Microsoft, and Crowdstrike. TLA+ doesn’t replace our engineering skill but augments it. With TLA+ we can design systems faster and more confidently. Check out the Conceptual Overview to see an example of this in practice. TLA+是一个“形式化验证语言”，是在完成系统设计之后，直接验证设计是否正确的手段。TLA+由图灵奖获得者Leslie Lamport开发，目前已经被多个大厂实践。TLA+并非用于代替工程技能，只是起到增强作用。利用TLA+，我们可以更快地完成系统设计，并对系统的质量更有把握。概念概述中包含更多实践上的例子。

关于本教程

This is a free online resource for learning TLA+. To help both beginners and experienced users, the guide is divided into three parts: 这是一个学习TLA+的免费在线资源。为了对初学者和有经验的老手都能够起到帮助作用，本教程分为三部分：

  • The Core: a linear introduction to all of the TLA+ language. It starts with basic operators and gradually progresses all the way to advanced topics. The core is intended to be read linearly: people new to TLA+ should start with the conceptual overview and then work forward from there. People comfortable with TLA+ should skim until they find new material. 核心：这部分是关于TLA+语言所有信息的直白（线性）的介绍。从基本的操作符开始，一直过渡到高阶的话题。对于TLA+新手，可以从概念概述开始，按顺序读完核心部分。对于TLA+老手，也可以按顺序略读这一部分，直到遇到不熟悉的内容。

  • Topics: “Optional” advanced material. Any individual lesson will be useful to many but not all TLA+ users. Unlike the core, these are designed to be mostly independent of each other. If topics have dependencies on other topics, I will call them out. 主题：“可选的”高阶教程。每一个章节都应该能对大多数TLA+使用者提供帮助，不过并不是所有TLA+使用者都能用得上。不同于核心部分，这一部分地不同章节基本上互相独立。如果不同章节之间存在依赖，教程中会给出相应提示。

  • Examples: Applications of TLA+ to specs, showing both how to write and understand specs. 示例：TLA+的在规约上的应用，呈现如何书写和理解规约。

This guide is still under development, check What’s New to see most recent updates and the roadmap to see what I’m currently working on.

关于作者

I’m Hillel. I’m part of the TLA+ foundation and the author of the book Practical TLA+. I wrote this because I want TLA+ to be as accessible as possible and didn’t like that my book cost money. I have a blog, a twitter, and a weekly newsletter. 作者Hilel，TLA+基金会的一员，《Practial TLA+》的作者。该教程旨在推广TLA+，且读起来不花钱。作者同时维护有博客、推特和周报。

(Full disclosure, I’m also a professional TLA+ consultant and <plug>run workshops</plug>.)

NextFAQ

Last updated