Zhang, Linpeng;
Kaminski, Benjamin Lucien;
(2022)
Quantitative Strongest Post:
A Calculus for Reasoning about the Flow of Quantitative Information.
In:
Proceedings of the ACM on Programming Languages.
ACM: Association for Computing Machinery
(In press).
Preview |
Text
2202.06765v1.pdf - Accepted Version Download (1MB) | Preview |
Abstract
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Quantitative Strongest Post: A Calculus for Reasoning about the Flow of Quantitative Information |
| Event: | OOPSLA 2022: ACM Conference on Systems, Programming, Languages, and Applications: Software for Humanity |
| Dates: | 14 Nov 2022 - 19 Nov 2022 |
| Open access status: | An open access version is available from UCL Discovery |
| Publisher version: | https://dl.acm.org/journal/pacmpl |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Incorrectness Logic, Quantitative Verification, Strongest Postcondition, Weakest Precondition |
| UCL classification: | UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science UCL > Provost and Vice Provost Offices > UCL BEAMS UCL |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10144577 |
Archive Staff Only
 |
View Item |
