预言变量

有些具体状态从过去看完全相同，未来却会迫使它们对应不同抽象状态。普通 refinement mapping 只能看当前状态，无法知道该选哪一个。预言变量把“后来会揭晓的答案”贴成一张 proof-only 标签，使映射现在就能引用它；运行程序并没有获得预知能力。

这张标签允许猜错。猜错的增广分支以后无法延伸，但同一原执行必须至少有一个猜对的标注，所以擦除标签后行为一条不少。若一开始只允许正确答案中的某一个，或者让程序按标签选择分支，就不再是证明辅助，而是把原系统偷偷改得更确定。

具体状态含一个待处理集合 $\{A,B\}$，未来操作 take 可以非确定地返回任一元素；抽象规格为了维护一个队列表示，必须更早确定“下一项”。加入 $p\in \{A,B\}$ 预测下一次返回。若具体轨迹后来返回 $B$，选择 $p=B$ 的增广轨迹可以继续，并把抽象队首映射为 $B$；选择 $p=A$ 的标注届时失效。由于原先返回 $A$、返回 $B$ 的两条轨迹分别都有一致标注，投影仍恰好得到原行为集。

若初始化规则只允许 $p=A$，返回 $B$ 的原行为没有扩展，投影变成真子集；用这个系统证明精化只证明了一个被删减的实现。若 take 在运行时读取 $p$ 并据此返回，同样改变了非确定选择的来源。正确用法是让 $p$ 约束辅助标注的合法性，而不是驱动实际变量或可见事件。

Herlihy–Wing 队列提供更真实的未来依赖：enqueue 先预留数组槽再填值，dequeue 的扫描与后来填槽交错，中间具体状态未必唯一决定抽象队列顺序。可为 pending dequeue 记录它将返回的槽或值，再构造状态映射。所需预言可能是一组索引或一段未来选择，不保证总是单个有限标量。

预言变量与 history variable 方向互补：history 记录已经发生的事件，prophecy 为尚未决定的抽象匹配提供未来信息。它可以把某些后向模拟转写为带辅助状态的前向 refinement mapping，但二者不是定义上的同义词；后向关系也可以直接保留多个抽象前驱而不显式添加变量。

有限操作结束后应消费、验证或更新相应预言；多个 pending 操作可能需要按请求标识维护一张预测表。把一个旧预测错误复用于下一次调用，会把不同未来选择绑定在一起，投影后可能删除原本独立的行为。

Abadi–Lamport 的完备性定理带有重要前提：在其行为语义下，若 machine-closed 的 $S_1$ 实现 internally continuous 且具有 finite invisible nondeterminism 的 $S_2$，则可先加 history variable、再加 prophecy variable，使 refinement mapping 存在。它不是“任何精化只要加一个预言标量都能证明”。无限行为、liveness 和 stuttering 会影响一致预言能否构造，必须保留原定理的技术条件。SMV 与 TLA+ 规格模式公理库SMV 与 TLA+ 规格模式SMV and TLA+ specification patterns · Symbolic and action-based specifications比较 SMV 的同步 next-state 关系与 TLA+ 的 action/stuttering 规格，并明确变量隐藏和公平性的工程边界。中的辅助变量实践也应接受同一投影保守性检查。