Abstract: We marry two seminal deductive program verification techniques: weakest pre-expectations (WPEs) and separation logic (SL). WPEs are a quantitative analogue of Dijkstra's weakest pre- conditions used to reason about probabilistic effects such as coin flipping. SL enables logical reasoning about pointer programs and can deal with aliasing, memory leaks, null pointer dereferencing etc.
We show that WPEs and SL can be combined in a natural and elegant way. The resulting quantitative separation logic (QSL) employs real-valued quantities instead of Boolean predicates and lifts the key SL connectives, separating conjunction and separating implication, from predicates to quantities.
We will argue that QSL conservatively extends both WPEs and SL. QSL’s wp-calculus is shown to be sound w.r.t. a simple operational semantics based on Markov decision processes, and preserves the frame rule, the key principle in SL enabling local reasoning about heaps.
QSL enables reasoning about quantities such as the probability of terminating with an empty heap, the expected length of a list returned by a lossy list reversal algorithm, or the expected length of a path from the root to a leaf in randomised meldable heaps.
QSL thus enables to reason about probabilistic programs mutating dynamic data structures in a compositional way purely at the source-code level.
