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.

翻译：我们提出了一个新的最强的限定条件式计算法,用于对非决定性程序进行循环定量推理。虽然现有的最弱的量化预言允许在程序终止后对某一初始状态下的数量值进行推理,但数量最强的日志允许对某数量在程序执行之前的价值进行推理,并达到某个最终状态。我们展示了最强的日志能够对通过程序进行的数量信息流动进行推理。与最弱的自由性先决条件相似,我们也开发了一个数量最强的自由性文章。作为一个副产品,我们获得了一个完全未探索的最强的自由性先决条件的概念,并展示了这些预示着一个潜在的新程序逻辑 — 部分错误逻辑 — — 将更自由地体现O'Hearn最近不正确的逻辑。