Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs

TL;DR

Quantitative separation logic ($\mathsf{QSL}$) extends classical separation logic by using real-valued quantities, enabling probabilistic reasoning about heap-manipulating programs with a sound calculus that preserves local reasoning.

Contribution

Introduction of $\mathsf{QSL}$, a conservative extension of classical separation logic with real-valued quantities, and development of a weakest precondition calculus for probabilistic programs.

Findings

Soundness proven with respect to Markov decision process semantics

Enables reasoning about probabilities of termination and reaching states

Preserves O'Hearn's frame rule for local reasoning

Abstract

We present quantitative separation logic ($\mathsf{QSL}$). In contrast to classical separation logic, $\mathsf{QSL}$ employs quantities which evaluate to real numbers instead of predicates which evaluate to Boolean values. The connectives of classical separation logic, separating conjunction and separating implication, are lifted from predicates to quantities. This extension is conservative: Both connectives are backward compatible to their classical analogs and obey the same laws, e.g. modus ponens, adjointness, etc. Furthermore, we develop a weakest precondition calculus for quantitative reasoning about probabilistic pointer programs in $\mathsf{QSL}$. This calculus is a conservative extension of both Reynolds' separation logic for heap-manipulating programs and Kozen's / McIver and Morgan's weakest preexpectations for probabilistic programs. Soundness is proven with respect to an operational semantics based on Markov decision processes. Our calculus preserves O'Hearn's frame rule, which enables local reasoning. We demonstrate that our calculus enables reasoning about quantities such as the probability of terminating with an empty heap, the probability of reaching a certain array permutation, or the expected length of a list.