Tractability of Separation Logic with Inductive Definitions: Beyond Lists
Tractability of Separation Logic with Inductive Definitions: Beyond Lists
复制标题
DOI：
10.4230/lipics.concur.2017.37
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Taolue Chen;Fu Song;Zhilin Wu
中科院分区：
文献类型：
--
作者：
Taolue Chen;Fu Song;Zhilin Wu
2011年，库克等人提出。证明了可以在多项式时间内检查分离逻辑片段的可满足性和蕴涵关系，该分离逻辑片段允许对具有指针和链表的程序进行推理。在这篇文章中，我们研究了可处理性结果是否可以扩展到更具表现力的分离逻辑片段，从而允许定义链表以外的数据结构。为此，我们引入了带有简单非线性组合归纳谓词的分离逻辑，其中源、目标和静态参数被显式地标识(SLID[SNC])。我们证明了如果归纳谓词有多个源(目的)参数，则SLID[SNC]的可满足性问题通常变得难以解决。这由用于双向链接列表段的归纳谓词来举例说明。相比之下，如果归纳谓词只有一个源(目标)参数，则SLID[SNC]的可满足性和蕴涵问题是容易处理的。特别是，可跟踪性结果适用于定义带有尾指针的列表段和带有一个洞的树的归纳谓词。
In 2011, Cook et al. showed that the satisfiability and entailment can be checked in polynomial time for a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. In this paper, we investigate whether the tractability results can be extended to more expressive fragments of separation logic that allow defining data structures beyond linked lists. To this end, we introduce separation logic with a simply-nonlinear compositional inductive predicate where source, destination, and static parameters are identified explicitly (SLID[snc]). We show that if the inductive predicate has more than one source (destination) parameter, the satisfiability problem for SLID[snc] becomes intractable in general. This is exemplified by an inductive predicate for doubly linked list segments. By contrast, if the inductive predicate has only one source (destination) parameter, the satisfiability and entailment problems for SLID[snc] are tractable. In particular, the tractability results hold for inductive predicates that define list segments with tail pointers and trees with one hole.