论文标题
定量最强的职位
Quantitative Strongest Post
论文作者
论文摘要
我们提出了一种新型的最强的条件风格的演算，用于与循环的非确定性程序进行定量推理。尽管现有的定量较弱的pre允许在程序终止在给定初始状态下终止数量的价值的推理，但定量最强的帖子允许对数量执行和达到给定的最终状态之前的数量进行推理。我们展示了最强的帖子如何通过程序来推理定量信息的流动。与最弱的自由主义前提类似，我们也开发了一个定量最强的自由派职位。作为副产品，我们获得了最强自由主义后条件的完全未开发的概念，并展示了这些预示着潜在的新程序逻辑 - 部分不正确的逻辑 - 这将是O'Hearn最近的错误逻辑的更为自由的版本。
We present a novel strongest-postcondition-style calculus for quantitative reasoning about non-deterministic programs with loops. Whereas existing quantitative weakest pre allows reasoning about the value of a quantity after a program terminates on a given initial state, quantitative strongest post allows reasoning about the value that a quantity had before the program was executed and reached a given final state. We show how strongest post enables reasoning about the flow of quantitative information through programs. Similarly to weakest liberal preconditions, we also develop a quantitative strongest liberal post. As a byproduct, we obtain the entirely unexplored notion of strongest liberal postconditions and show how these foreshadow a potential new program logic - partial incorrectness logic - which would be a more liberal version of O'Hearn's recent incorrectness logic.
