TLA+是什么
作者：互联网
对于一套系统的设计，通常我都是想好了，然后直接捋起袖子写代码了。
写完了，在开始加很多 test 来保证它的正确性。
但其实，我并不能保证设计是完全正确的。也就是说，我的实现满足了该系统的需求，但也有可能在一些 corner case 上面并没有考虑周全。
同时， 虽然后面可以写很多 test，但并不一定能 cover 到所有的分支。
所以，为了更好的确保设计的正确性，我们需要使用 TLA+ 或者其他类似的工具。
TLA+ 是一门形式规格说明语言(formal specification language)，主要用来验证系统的设计和算法的正确性。
TLA+ 是对系统（譬如程序，算法，操作系统等）更高层的建模，但 TLA+ 并不能生产任何代码。
对于很多程序员来说，首要直觉这是这玩意到底有啥用？
TLA+ 可以认为是一种新的思考方式，是在代码之上更上层的规格说明。
通过 TLA+ 来设计系统，能让我们更好的对整个系统进行抽象。
详细请看
https://www.jianshu.com/p/a5aaed054f40
标签：什么,系统,正确性,TLA,test,设计,代码 来源： https://blog.csdn.net/u013288190/article/details/115523198