1
条回答
写回答
写回答
-
TLA+在学术界和工业界都有着广泛的应用。TLA+ Examples给出了一些使用TLA+验证过的分布式算法和并发算法。在分布式算法和并发算法的研究领域，提出一个新的算法或者改进一个现有的算法，TLA+验证基本是标配。很多分布式算法论文在非形式化的论证介绍之外, 会附带TLA+的Specification来证明自己的算法是经过形式化验证的。对TLA+比较熟悉的业内人士来说，直接看TLA+的Specification甚至比看大段的论文理解的更快，对于论文的语言描述没有看明白，或者觉得有歧义的时候，查看TLA+的Specification对照着理解，有时候是阅读论文的一把利器，甚至有时候一些算法细节只能在TLA+的Specification里看到。由于Specification是逻辑严密滴水不漏的，可以更好的作为实现的指导。
2022-05-10 14:46:22赞同 展开评论 打赏
版权声明：本文内容由阿里云实名注册用户自发贡献，版权归原作者所有，阿里云开发者社区不拥有其著作权，亦不承担相应法律责任。具体规则请查看《阿里云开发者社区用户服务协议》和《阿里云开发者社区知识产权保护指引》。如果您发现本社区中有涉嫌抄袭的内容，填写侵权投诉表单进行举报，一经查实，本社区将立刻删除涉嫌侵权内容。
相关问答
