TLA+

现在我们有了我们的脚手架PlusCal，是时候学习TLA+了。TLA+是一种数学描述语言。不是说如何找到你想要的值，而是说你想要的属性。例如，集合中最大的元素是CHOOSE x \in S : \A y \in S : y <= x，这不是一个算法，它只是“比其他数字大的数字。”

这给了我们惊人的规格能力。复杂的属性和不变量可以用几行来表示。不利的一面是，它也可能非常令人生畏。也有可能意外地构建不可检查的模型。例如，很容易定义所有停止的通用图灵机器的集合。但是，如果您将它输入到TLC，它将返回一个错误。写TLA+ spec有点艺术。让我们开始吧。

注意事项:我们将几乎完全忽略“时间逻辑”的“暂时”部分。作为一种简单的启发式，我们永远不会讨论“启动和非启动操作符”，这大约占指定系统的95%。在它的核心，TLA+是一个优美的方式来优雅地表达一个复杂系统的时间属性。对于我们的使用，TLA+是一种编写更好的plus spec的方法。Sacriligious吗?可能。容易吗?是的。