一句话：提出定量分离逻辑 QSL，为概率指针程序提供带局部推理的定量最弱前置条件演算。
论文提出定量分离逻辑（QSL），将经典分离逻辑中的谓词提升为取实数值的定量，并相应提升分离合取与分离蕴涵。该扩展保守兼容经典分离逻辑，并保持 modus ponens、伴随性等定律。作者进一步建立面向概率指针程序的最弱前置条件演算，它同时保守扩展了 Ishtiaq/O'Hearn/Reynolds 的堆程序分离逻辑与 Kozen/McIver-Morgan 的概率最弱前置期望。基于 Markov 决策过程操作语义证明了演算的可靠性，并保留 O'Hearn 的帧规则以支持局部推理。案例表明可推理终止时堆为空的概率、到达某数组排列的概率以及链表期望长度等定量性质。
We present quantitative separation logic (QSL). In contrast to classical separation logic, 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 QSL. This calculus is a conservative extension of both Ishtiaq’s, O’Hearn’s and 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.
@article{paperbot647,
title = {Quantitative separation logic: a logic for reasoning about probabilistic pointer programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290347}
}