AI 中文总结
研究提出用预言变量解决程序分析问题，通过特定语言指定变量，紧密耦合变量规范与操作语义，消除传统机制。给出预言和历史变量的验证实现，证明经典转换的正确性和最优性，是首批此类机器检查证明。
AI 中文摘要
我们提出了预言变量，用于程序分析问题的前向公式，这些问题需要有关程序未来执行的信息。我们通过一种领域特定语言来指定预言和历史变量，该语言通过对预言和历史变量的子集包含约束来增强基本操作语义的步骤规则。预言和历史变量规范与操作语义之间的这种紧密耦合促进了程序转换的正确性和最优性证明的构建，证明结构为程序原始版本和转换版本之间的前向模拟。与传统数据流方法相比，这种方法消除了诸如显式控制流图、抽象函数、具体化函数、伽罗瓦连接以及单独的向后和向前分析等机制。我们展示了预言和历史变量的经过验证的实现，并使用该实现来证明两个经典转换（部分死代码消除和惰性代码移动）的正确性和最优性属性，这两个转换都使用了预言和历史变量。据我们所知，这些证明是这些转换的首批机器检查的正确性和最优性证明。
英文摘要
We present prophecy variables for forward formulations of program analysis problems that require information about the future execution of the program. We specify prophecy and history variables via a domain specific language that augments the step rules of the base operational semantics with subset inclusion constraints over the prophecy and history variables. This tight coupling between the prophecy and history variable specification and the operational semantics promotes the construction of correctness and optimality proofs for program transformations, with the proofs structured as forward simulations between the original and transformed versions of the program. In comparison with traditional dataflow approaches, this approach eliminates mechanisms such as explicit control flow graphs, abstraction functions, concretization functions, Galois connections, and separate backward and forward analyses. We present a verified implementation of prophecy and history variables and use the implementation to prove correctness and optimality properties of two classic transformations, partial dead code elimination and lazy code motion, that use both prophecy and history variables. To the best of our knowledge, these proofs are the first machine checked correctness and optimality proofs for these transformations.
