  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.
