山东省建设注册执业中心网站,云南微网站搭建,达内网站开发视频教程,第三方网站0x01 TLA是个好工具
编程人员一个好习惯是凡事都想偷懒#xff0c;当然是指要科学地偷懒#xff0c;而不是真的偷懒。一直想找到一种能检验写出的代码#xff0c;做出的设计是否真的完全正确#xff0c;而不是靠经验检视、代码Review、反复测试去检验。因为上述方法不管怎…0x01 TLA是个好工具
编程人员一个好习惯是凡事都想偷懒当然是指要科学地偷懒而不是真的偷懒。一直想找到一种能检验写出的代码做出的设计是否真的完全正确而不是靠经验检视、代码Review、反复测试去检验。因为上述方法不管怎么努力都有可能受限于各种条件而无法给出可靠的结论而且还要花费大量精力。想来想去可行的方式就是用一种高层次的抽象模型去描述、模拟整个系统这样就能以较低的成本达成这样的效果。个人水平有限还没想出这种语言应该是什么样子的。直到看到了TLA。
初步学习了下发现这正是我想找的工具。 对编码和设计来说”偷懒到起点提前做正确性评估“。
TLA是每个做分布式或并发系统开发人员都应该学习的工具。它由牛人Leslie LamportPaxos算法的作者开发的专门用于分布式算法验证的工具。对于软件开发者来说它就是所有工具中的”终极武器“。
但不是每个人都必须学的。它确实对使用者有要求。
系统抽象能力。最终模型的好坏取决于使用者对系统的抽象质量开发经验少的人可能不太适合。数学基础。TLA出的模型就是一页页的数学公式数学基础不好看见公式就头疼的人可能也不太适合当然可以使用 PlusCal语言减小这一个要求但想发挥TLA全部能力还是建议直接使用TLA。
AWS用它检验关键服务、分布式算法的正确性发现了许多常规手段无法发现的疑难BUG包含可能导致用户数据丢失的严重问题。开源社区用它检查分布式算法比如ZooKeeper社区也使用它检查FLE、ZAB协议。甚至有人能用它检查一段有隐晦BUG的Go代码。阿里云也在用它检查关键算法的正确性。
详细介绍可以见参考章节首页链接。 0x02 Hello World
一个合法的Hello Word PlusCal算法如下。
------------------------------ MODULE Session2 ------------------------------
EXTENDS TLC
(* --algorithm Basic1variables x 1;begin
print hello world;
end algorithm; *)------- MODULE Session2 -------行是Spec的命名必须要有新建Spec时自动生成的。EXTENDS TLC 是引入TLC组件因为print语句在其中定义。(* * 是注释块包含了CalPlus算法--algorithm Basic1是算法的开始CalPlus以注释寄存在TLA的Spec中。Basic1是算法名称可以是合法的TLA名称字符。variables 为声明变量行。这里不是必须的因为我们没用到。begin 必须要有是声明具体语句的开始。print x 打印x的内容。end algorithm 表示算法结束。必须有是声明与TLA的分割。 按Ctrl-T转换为TLA后即新建 Model后运行就可以在User Output框中看到输出了。 0x04 学习方式
通过PlusCal还是直接上手TLA看个人吧。数学基础好一点可以考虑直接上手TLA但如果是考虑在团队中推广则从PlusCal比较好可以照顾到团队中的大多数人。 0x05 参考
TLA主页 https://lamport.azurewebsites.net/tla/tla.html
欢迎关注订阅号
