Extended transitive separation logic
Extended transitive separation logic
复制标题
DOI：
10.1016/j.jlamp.2014.12.002
复制
发表时间：
2015-05
期刊：
影响因子：
--
通讯作者：
Han-Hing Dang;B. Möller
中科院分区：
文献类型：
--
作者：
Han-Hing Dang;B. Möller
分离逻辑（英语：Separation logic，SL）是霍尔逻辑的一个扩展，通过运算符和公式来更灵活地推理堆部分或链接的对象/记录结构。在本文中，我们给SL的代数扩展的数据结构的水平。同时，我们超越了标准SL，不仅研究堆部分的域不相交性，而且研究沿着传递链接的不相交性。为此，我们定义的操作，允许表达有关链接结构的假设。待处理的现象包括可达性分析，（缺乏）共享，循环检测和保存下破坏性分配的子结构。我们证明了这种方法的实用性，在现场列表反转，树旋转和线程树的例子。
Separation logic (SL) is an extension of Hoare logic by operators and formulas for reasoning more flexibly about heap portions or linked object/record structures. In the present paper we give an algebraic extension of SL at the data structure level. At the same time we step beyond standard SL by studying not only domain disjointness of heap portions but also disjointness along transitive links. To this end we define operations that allow expressing assumptions about the linking structure. Phenomena to be treated comprise reachability analysis, (absence of) sharing, cycle detection and preservation of substructures under destructive assignments. We demonstrate the practicality of this approach with examples of in-place list-reversal, tree rotation and threaded trees.