Prophecy Made Simple
ACM Transactions on Programming Languages and Systems(2022)
摘要
AbstractProphecy 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.
更多查看译文
关键词
Formal specification, state machine, refinement, auxiliary variable
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要