paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Prophecy Made Simple

让预言变量变得简单
TOPLAS 44(2)2022匹配度 2/10 · 该论文属于程序验证与形式语义领域，讨论预言变量与精化映射的数学化重构，与用户核心方向中的 LLM/Agent 结合静态分析、浮点程序分析或贝叶斯程序分析均无直接关联。引用 9 inbox
Leslie Lamport, Stephan Merz
程序验证形式语义
crossref: 2026-09-10

AI 速览

一句话：提出一种更易使用的新型预言变量，并以更数学化的方式重新表述精化映射理论。

预言变量由 Abadi 和 Lamport 在《The Existence of Refinement Mappings》一文中引入，用于精化映射的存在性证明，但在实践中难以使用。本文提出一种新型预言变量，作者认为其使用起来简单得多。同时，文章将原文中的相关思想以更数学化的方式重新表述，使精化映射与预言变量的理论更清晰。摘要未给出实验评估；工作属于理论/方法层面的简化与重构。

问题
预言变量虽在 Abadi-Lamport 的精化映射工作中被引入，但原有形式在实践中难以使用。
方法
作者定义了一种新型预言变量，并重新以更数学化的方式表述原文思想。
评估
摘要未报告实验或案例评估，工作以概念定义与理论重述为主。
原文摘要（Abstract）

Prophecy variables were introduced in the article “The Existence of Refinement Mappings” by Abadi and Lamport. They were difficult to use in practice. We describe a new kind of prophecy variable that we find much easier to use. We also reformulate ideas from that article in a more mathematical way.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot1618,
  title = {Prophecy Made Simple},
  author = {Leslie Lamport and Stephan Merz},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {44},
  number = {2},
  year = {2022},
  doi = {10.1145/3492545}
}