0x01 TLA+是个好工具

编程人员一个好习惯是凡事都想偷懒，当然是指要科学地偷懒，而不是真的偷懒。一直想找到一种能检验写出的代码，做出的设计是否真的完全正确，而不是靠经验检视、代码Review、反复测试去检验。因为上述方法不管怎么努力都有可能受限于各种条件而无法给出可靠的结论，而且还要花费大量精力。想来想去可行的方式就是用一种高层次的抽象模型去描述、模拟整个系统，这样就能以较低的成本达成这样的效果。个人水平有限，还没想出这种语言应该是什么样子的。直到看到了TLA+。

初步学习了下，发现这正是我想找的工具。 对编码和设计来说，”偷懒到起点提前做正确性评估“。

TLA+是每个做分布式或并发系统开发人员都应该学习的工具。它由牛人Leslie Lamport（Paxos算法的作者）开发的，专门用于分布式算法验证的工具。对于软件开发者来说，它就是所有工具中的”终极武器“。

但不是每个人都必须学的。它确实对使用者有要求。

1. 系统抽象能力。最终模型的好坏取决于使用者对系统的抽象质量，开发经验少的人可能不太适合。
2. 数学基础。TLA+出的模型就是一页页的数学公式，数学基础不好看见公式就头疼的人可能也不太适合，当然可以使用 PlusCal语言减小这一个要求，但想发挥TLA+全部能力，还是建议直接使用TLA+。

AWS用它检验关键服务、分布式算法的正确性，发现了许多常规手段无法发现的疑难BUG，包含可能导致用户数据丢失的严重问题。开源社区用它检查分布式算法，比如ZooKeeper社区也使用它，检查FLE、ZAB协议。甚至有人能用它检查一段有隐晦BUG的Go代码。阿里云也在用它，检查关键算法的正确性。

详细介绍可以见参考章节首页链接。

0x02 Hello World

一个合法的Hello Word PlusCal算法如下。

------------------------------ MODULE Session2 ------------------------------
EXTENDS TLC
(* --algorithm Basic1

variables x = 1;

begin
print "hello world";
end algorithm; *)
====

1. ------- MODULE Session2 -------行是Spec的命名，必须要有，新建Spec时自动生成的。
2. EXTENDS TLC 是引入TLC组件，因为print语句在其中定义。
3. (* *） 是注释块，包含了CalPlus算法，--algorithm Basic1是算法的开始，CalPlus以注释寄存在TLA+的Spec中。Basic1是算法名称，可以是合法的TLA+名称字符。
4. variables 为声明变量行。这里不是必须的，因为我们没用到。
5. begin 必须要有，是声明具体语句的开始。
6. print x 打印x的内容。
7. end algorithm； 表示算法结束。
8. ====必须有，是声明与TLA+的分割。

按Ctrl-T转换为TLA+后，即新建 Model后，运行，就可以在User Output框中看到输出了。

0x04 学习方式

通过PlusCal还是直接上手TLA+，看个人吧。数学基础好一点可以考虑直接上手TLA+，但如果是考虑在团队中推广，则从PlusCal比较好，可以照顾到团队中的大多数人。

0x05 参考

1. TLA+主页 https://lamport.azurewebsites.net/tla/tla.html

欢迎关注订阅号