Fictional Separation Logic
Fictional Separation Logic
复制标题
DOI：
10.1007/978-3-642-28869-2_19
复制
发表时间：
2012-03
期刊：
影响因子：
--
通讯作者：
J. B. Jensen;L. Birkedal
中科院分区：
文献类型：
--
作者：
J. B. Jensen;L. Birkedal
分离逻辑通过框架规则和分离合取P*Q来形式化堆操作程序的局部推理的思想，分离合取P*Q描述了可以被分成几个部分的状态，其中一个满足P，另一个满足Q。在标准分离逻辑中，分离意味着物理分离。本文介绍了虚拟分离逻辑，它包含了更一般形式的虚拟分离连词P*Q，其中*不需要物理分离，但也可以用于PQ描述的内存资源重叠的情况。我们通过一系列示例演示了如何使用虚构的分离逻辑来本地和模块化地推理可变的抽象数据类型，可能使用复杂的共享来实现。虚拟分离逻辑是在标准分离逻辑的基础上定义的，其元理论和应用都比以前的相关方法简单得多。
Separation logic formalizes the idea of local reasoning for heap-manipulating programs via the frame rule and the separating conjunctionP*Q, which describes states that can be split intoseparateparts, with one satisfyingPand the other satisfyingQ. In standard separation logic, separation means physical separation. In this paper, we introducefictional separation logic, which includes more general forms of fictional separating conjunctionsP*Q, where * does not require physical separation, but may also be used in situations where the memory resources described byPandQoverlap. We demonstrate, via a range of examples, how fictional separation logic can be used to reason locally and modularly about mutable abstract data types, possibly implemented using sophisticated sharing. Fictional separation logic is defined on top of standard separation logic, and both the meta-theory and the application of the logic is much simpler than earlier related approaches.