编译器后向模拟

后向模拟像审查已经生成的机器执行：目标每做一件可见或内部工作，都要回到源模型找到合法来历。因为调查从目标路径开始，目标若多出一个崩溃、输出或分支，证明会立即卡住；这与“目标不能新增行为”的安全诉求方向一致。

“后向”说的是匹配责任，不是倒放时间。源仍从初态向后继前进，目标也向后继前进；只是全称量化首先挑目标步，再要求源追上。把箭头真的逆转会得到前驱可达性问题，不是编译器 backward simulation。

设源把赋值拆成求值与写回两步，目标用一条原子加法指令完成 $x:=x+1$。目标从 $q$ 一步到 $q^{\prime }$ 时，源从相关状态 $s$ 先算出临时值，再写回，两步迹均为空并到达 $s^{\prime }$，且新环境中的 $x$ 相等。因此一个目标步可由源若干步匹配；步数不相等不妨碍行为包含。

静默停顿反例取目标状态 $q_0\to q_1\to q_2\to \cdots$，每步无事件，而源状态 $s$ 已经终止。若允许每个目标步都由源零步匹配并始终令 $R(s,q_i)$，形式上的局部菱形成立，却把目标发散伪装成源终止。要求自然数阶段随零步匹配严格下降会排除此证明，因为不存在无限下降链。

后向模拟也不自动保留源的全部选择。若源可返回 $0$ 或 $1$，目标固定返回 $0$，每条目标行为都有源见证，后向模拟成立；这正是合法消除非确定性。若应用还要求概率分布、公平性或“每个源选择都可实现”，必须采用更强观察或双向性质。

后向模拟适合直接组合成目标行为精化，但构造关系有时比前向归纳困难，尤其当源非确定步骤必须在看到目标后继后选择。标准编译验证常先建立较自然的编译器前向模拟公理库编译器前向模拟Compiler forward simulation · Forward simulation proof for compilers · 编译正确性的前向模拟以源状态到目标状态的关系逐步匹配每个源执行步，并用正步进展或良基度量约束静默停顿。，再在源 receptive、目标 determinate、初终态与迹条件满足时应用转换定理。条件是定理的一部分，不能只引用“确定性”一个词。

receptiveness 处理环境事件的选择：若目标能接受某个输入事件，源在相同历史下也应能以兼容事件继续；determinacy 则约束目标从同一状态的可见选择及静默步。它们共同帮助把“源挑一步、目标跟随”的前向见证重排为“目标先走、源解释”的后向见证。普通内部非确定性若不满足这些性质，重排可能失败。

多阶段后向模拟的复合还需处理中间层的静默发散。若每段都允许 stuttering，简单关系复合可能找不到一个共同下降度量；常用词典序或阶段索引组合，但必须证明良基。对于 UB，源一旦进入允许任意行为的顶部，后续目标匹配可以宽松；在此之前仍需逐步维持关系。