Quantitative strongest post: a calculus for reasoning about the flow of quantitative information
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.
Thu 8 DecDisplayed time zone: Auckland, Wellington change
15:30 - 17:00 | |||
15:30 30mTalk | Checking Equivalence in a Non-strict Language OOPSLA DOI | ||
16:00 30mTalk | Necessity Specifications for Robustness OOPSLA Julian Mackay Victoria University of Wellington, Susan Eisenbach Imperial College London, James Noble Research & Programming, Sophia Drossopoulou Meta and Imperial College London DOI | ||
16:30 30mResearch paper | Quantitative strongest post: a calculus for reasoning about the flow of quantitative information OOPSLA Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University and University College London DOI |