Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
复制标题
DOI：
10.1145/3290347
复制
发表时间：
2018-02
影响因子：
--
通讯作者：
Kevin Batz;Benjamin Lucien Kaminski;J. Katoen;Christoph Matheja;T. Noll
中科院分区：
文献类型：
--
作者：
Kevin Batz;Benjamin Lucien Kaminski;J. Katoen;Christoph Matheja;T. Noll
我们提出了定量分离逻辑（QSL）。与经典的分离逻辑相反，QSL使用计算为真实的数的量，而不是计算为布尔值的谓词。经典分离逻辑的连接词分离合取和分离蕴涵是从谓词提升到量的。这个扩展是保守的：这两个连接词是向后兼容的经典类似物，并遵守相同的法律，例如，肯定前件，伴随性等。此外，我们开发了一个最弱的前提演算定量推理概率指针程序在QSL。这种演算是Ishtiaq、O 'Hearn和Reynolds的堆操作程序分离逻辑和Kozen/ McIver和Morgan的概率程序最弱预期望的保守扩展。可靠性证明相对于马尔可夫决策过程的基础上的操作语义。我们的演算保留了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.