# Quantitative Strongest Post

arXiv: https://arxiv.org/abs/2202.06765 · HTML: https://mlsanity.com/paper/2202.06765/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Feb 2022.

## Built on by (most cited first, 1 of 1)

- [Weighted Programming](https://mlsanity.com/paper/2202.07577/) (2022)

## Abstract (arXiv)

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.