In this repository we verify the quantitative Separation Logic following the paper Quantitative Separation Logic by Batz et al. [1]
The current theories are developed with Isabelle 2020.
-
Theory Quantitative_Separating_Connectives defines quantitative versions of the separating conjunction and magic wand. Also it generalizes the notion to arbitrary quantales. For the boolean quantale
(bool,==>,/\,<==)this simplifies to normal separation logic, for the quantale(ennreal,<=,*,/)we obtain the quantitative separation logic from -
In Theory HPGCL we define the deeply embedded heap-manipulating guarded command language (hpGCL)
-
We instantiate that general framework for
- Potentials in QSL_For_Potentials
- Probabilities in QSL_For_Probabilities
- Expectations in QSL_For_Expectations
[1] Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll, Quantitative Separation Logic, POPL, 2019. Technical Report