Quantitative Separation Logic

Origin. Batz, Kaminski, Katoen, Matheja, and Noll, "Quantitative separation logic: a logic for reasoning about probabilistic pointer programs" (POPL 2019; arXiv:1802.10467). It joins two lines that had stayed apart: Ishtiaq, O'Hearn, and Reynolds' separation logic for heap manipulation, and Kozen's and McIver and Morgan's weakest preexpectations for probabilistic programs. Extended to concurrency by Fesefeldt, Katoen, and Noll (CONCUR 2022). Not to be confused with Atkey's quantitative type theory, nor with his amortised resource analysis in separation logic — different systems with adjacent names.

Models. Assertions are quantities, not predicates: an assertion is a map from states (stack together with heap) to ℝ≥0 ∪ {∞}, an expectation in the Kozen sense. Classical separation logic sits inside as the {0,1}-valued fragment, each classical formula entering as its Iverson bracket. What one proves is therefore an expected value rather than a truth: the probability of terminating with an empty heap, the expected length of a list, the probability of reaching a given array permutation.

Formalism.

Expectations: 𝔼 = the set of maps f : States → ℝ≥0 ∪ {∞}, ordered pointwise. A complete lattice, which is what makes fixed points for loops available. [φ]: the Iverson bracket of a classical assertion φ — 1 where φ holds, 0 elsewhere.

Quantitative separating conjunction: (f ⋆ g)(s, h) = sup { f(s, h₁) · g(s, h₂) | h₁ ⊎ h₂ = h } The classical existential over splittings becomes a supremum, and conjunction becomes multiplication. On Iverson brackets it collapses to the classical connective: [φ] ⋆ [ψ] = [φ * ψ].

Quantitative separating implication: (f −⋆ g)(s, h) = inf over heaps h′ disjoint from h of the residual of g(s, h ⊎ h′) against f(s, h′). Chosen so that adjointness survives: f ⋆ − is left adjoint to f −⋆ −, which is the quantitative form of the classical modus ponens f * (f −⋆ g) ⊢ g.

Conservativity: Both connectives are backward compatible and obey the classical laws — commutativity, associativity, adjointness, modus ponens. QSL as an assertion language is a conservative extension of classical separation logic.

Weakest preexpectation: wp⟦C⟧(f) = the expected value of f after running C, as a function of the initial state. wp⟦x := e⟧(f) = f[x/e] wp⟦C₁; C₂⟧(f) = wp⟦C₁⟧(wp⟦C₂⟧(f)) wp⟦{C₁} [p] {C₂}⟧(f) = p · wp⟦C₁⟧(f) + (1 − p) · wp⟦C₂⟧(f) Loops are least fixed points; wp is Scott-continuous, so they exist. wlp is the separate dual for partial correctness, on expectations bounded by 1.

Frame rule: If C does not modify the free variables of g: wp⟦C⟧(f) ⋆ g ⊑ wp⟦C⟧(f ⋆ g) Local reasoning is preserved — this is the point of building on separation logic rather than beside it.

Symbols.

Metatheory. Conservative in both directions, which is the paper's main claim on the reader's attention: restrict the expectations to {0,1} and QSL is separation logic; drop the heap and it is the weakest-preexpectation calculus. Soundness is proved against an operational semantics given by Markov decision processes. The frame rule survives the lift, so locality is not paid for. Expectations form a complete lattice under the pointwise order, giving least fixed points for loops and Scott-continuity of wp. The absence of Boolean negation is structural, not an oversight — non-negative reals have no complement — and is why total and partial correctness need the separate calculi wp and wlp.

Applies to. Probabilistic pointer programs. Randomized data structures: skip lists, randomized binary search trees, randomized splay trees. Expected running time and expected resource consumption of heap-manipulating code. Average-case analysis where the heap shape is itself random.

Limitations. Loop reasoning needs quantitative invariants, which are harder to guess than Boolean ones and rarely inferrable. Unbounded expectations force care with suprema and infima, and the bounded fragment is where most of the clean theory lives. No negation, hence two calculi rather than one. Automation is immature relative to classical separation logic's, where entailment fragments are decidable and tooled.

© 2026 Lingenic LLC