Quantitative Separation Logic – A Logic for Reasoning about Probabilistic Pointer Programs

We present quantitative separation logic (QSL). In contrast to classical separation logic, QSL employs quantities which evaluate to non-negative real numbers instead of predicates which evaluate to boolean values. The characteristic connectives of classical separation logic, separating conjunction (*) and separating implication (–*), are both 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 of * and –*, etc. Furthermore, we develop a weakest precondition calculus for quantitative reasoning about probabilistic pointer programs in QSL. This calculus is a conservative extension of both Reynolds’ weakest preconditions for heap manipulating programs and McIver & Morgan’s weakest preexpectations for probabilistic programs. In particular, our calculus preserves the frame rule which enables local reasoning – a key principle of separation logic. Joint work with Kevin Batz, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll.

Authors

• Benjamin Lucien Kaminski.

Keywords

No keywords are indexed for this paper.