当语言实现破坏语言保证时，人们会感到困惑People get confused when language implementations break language guarantees

请看下面的 Python 程序：

# x = 1, y = 2
x = 0
y = x
print([x, y])

它会输出 [0, 0]。如果我们交换两个赋值语句，则会输出 [0, 1]。每个赋值都发生在独立的时间步中。几乎所有命令式语言都是这样工作的。

现在来看一个 TLA+ 代码片段：

\* x = 1, y = 2
/\ x' = 0
/\ y' = x
/\ PrintT(<<x', y'>>)

这会输出 <<0, 1>>。与命令式语言不同，TLA+ 将更新和时序步骤的概念进行了分离。我们读作 x' = 0 表示“在下一个状态中，x 将是 0，但在当前状态中它仍保持原有值”。因此，在每个状态下，x 和 x' 本质上是独立的变量。由于这个原因，在 TLA+ 语义中语句的顺序无关紧要，交换两个赋值语句不会改变输出结果。这个语言设计得真巧妙！这意味着基本上不存在单步内的竞态条件。一个函数可以更新某个变量而不影响其他函数如何使用它。

好了，现在初学者不可避免地会遇到一个问题：

\* x = 1, y = 2
/\ x' = y'
/\ y' = x
/\ PrintT(<<x', y'>>)

这会导致崩溃，因为 y' 尚未定义。但如果我们交换两个赋值语句，则可以正常工作并输出 <<1, 1>>。所以显然关于非顺序性的说法完全是胡扯。

不完全是这样。TLA+ 语义仍然保证非顺序性。问题在于验证器并未完美实现 TLA+ 语义。y' > 0 是一个完全合理的“赋值”，但存在无限多个可能的下一状态！因此主模型检查器（TLC）要求 y' = some_value 必须在任何其他使用 y' 之前出现，这意味着现在顺序变得重要了。

更大的问题是 PrintT。TLA+ 语义之所以保证非顺序性，是因为语义不允许副作用的存在。而模型检查器引入了具有副作用的操作符如 PrintT、Assert 和 IOExec，这可能导致守卫语句出现问题。从理论上讲这两个脚本块是等价的：

/\ x = 0 \* guard statement
/\ P()
/\ x' = x + 1

/\ x' = x + 1
/\ P()
/\ x = 0 \* guard statement

当 x = 1 时，这些不会导致新状态的产生，因为存在守卫子句。但模型检查器逐行评估每一行代码，意味着在第二个块中，它会在到达 x = 0 并丢弃状态之前先执行 x' = x + 1 和 P()。如果 P 是一个标准的 TLA+ 操作符，则这不是问题；但如果它是 PrintT 或 Assert，则其效果会首先生效，从而导致一些奇怪的现象——打印出与任何下一个状态都不对应的幽灵输出。

“TLA+ 语义所保证的内容”与“TLC 破坏这些保证的具体方式”之间的差异，是许多人感到困惑的巨大来源！此外，许多这样的操作符，比如 IOExec 和 TLCSet，本意就是作为逃生舱口。所以如果你需要使用它们，说明你已经在做一些相当奇怪的事情，这就让情况变得更加混乱。

更糟糕的是，没有任何语法或视觉上的区别能够区分破坏保证的 TLC 操作符和常规安全的 TLA+ 操作符。在编译型语言中有预处理器和指令（pragma），允许编译器做语言本身无法做到的事。但这些通常都有明显不同的语法，让你一眼就能看出这里有危险。

这让我想起了 Neel Krishnaswami 那篇令人惊叹的文章《什么是声明式语言》：

这也让我们可以做出预测：任何声明式语言中最不受欢迎的特性，往往是那些暴露操作模型并破坏声明式语义的功能。因此我们可以预测人们会不喜欢（a）正则表达式中的反向引用，（b）语法分析中的有序选择，（c）查询语言中的行 ID，（d）Prolog 中的截断（cut），（e）约束语言中的约束优先级。

截断操作具有视觉上明显不同的语法形式，但使用截断的谓词在外观上与逻辑纯净的谓词并无区别。不过，这比我们在 TLA+ 中遇到的情况稍微简单一些，因为截断仍然是语言语义的一部分。

（话虽如此，不同 Prolog 方言在字符串打印方面有不同的处理方式，这些操作会给 Prolog 带来副作用，而且它们与其他谓词在外观上也无法区分。所以问题依旧！）

我实际上并没有解决这个问题的方案。我只是觉得这是一个有趣的“抽象泄漏”案例。也许我们可以编写一个代码高亮工具，将所有间接使用“奇怪”函数的函数高亮显示出来。