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.

Symbol	Unicode	Name	Meaning
⋆	U+22C6	Star operator / Quantitative separating conjunction	Supremum over heap splittings of a product
−⋆	—	Quantitative magic wand	Right adjoint to ⋆ (minus sign plus star operator)
*	U+002A	Asterisk / Classical separating conjunction	The Boolean connective ⋆ generalizes
↦	U+21A6	Rightwards arrow from bar / Points-to	Singleton heap cell
[φ]	—	Iverson bracket	1 where the classical assertion φ holds, 0 elsewhere
𝔼	U+1D53C	Double-struck capital E / Expectations	Maps States → ℝ≥0 ∪ {∞}
ℝ	U+211D	Double-struck capital R / Reals	Codomain of an expectation
∞	U+221E	Infinity	Top of the expectation lattice
⊎	U+228E	Multiset union / Disjoint heap union	h₁ ⊎ h₂ defined when the domains are disjoint
·	U+00B7	Middle dot / Multiplication	Product of expectations; probabilistic weighting
⟦	U+27E6	Left white square bracket	Opens the semantic bracket in wp⟦C⟧
⟧	U+27E7	Right white square bracket	Closes the semantic bracket
⊑	U+2291	Square image of or equal to / Pointwise order	f ⊑ g pointwise on states
wp	—	Weakest preexpectation	Expected value of f after C
wlp	—	Weakest liberal preexpectation	Partial-correctness dual, on expectations ≤ 1
sup, inf	—	Supremum, infimum	Defining ⋆ and −⋆ over heap splittings

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 lost. 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. There is no Boolean negation on expectations, since the non-negative reals have no complement; wlp is therefore not obtainable from wp by dualising, and total and partial correctness require two calculi that must be developed and applied separately. Loop reasoning bottoms out in a least fixed point that the calculus cannot name, so a quantitative invariant — a super-invariant for wp or a sub-invariant for wlp — must be supplied, and the underlying decision problem is severe: Kaminski and Katoen (2015) placed almost-sure termination of probabilistic programs at Π⁰₂-complete and positive almost-sure termination at Σ⁰₂-complete, so these questions are not merely undecidable but beyond the arithmetical level at which semi-decision procedures live. Both new connectives are defined by suprema and infima over heap splittings, and for unbounded expectations these need not be attained, so no witnessing splitting is available to a proof search. Entailment f ⊑ g subsumes classical separation logic entailment and adds real arithmetic on top of it, so it is undecidable once quantifiers are present.