Completeness for Recursive Procedures in Separation Logic
Completeness for Recursive Procedures in Separation Logic
复制标题
分离逻辑中递归过程的完整性
DOI：
10.1016/j.tcs.2016.04.004
复制
发表时间：
2016
影响因子：
1.1
通讯作者：
Mahmudul Faisal Al Ameen and Makoto Tatsuta
中科院分区：
文献类型：
--
作者：
櫻井優太;関川浩;Mahmudul Faisal Al Ameen and Makoto Tatsuta
本文证明了Hoare逻辑和分离逻辑的一个推广对于具有相互递归过程的指针程序的完备性。本文还展示了断言语言的表达能力。本文通过引入两个新的推理规则实现了一个新的系统，并去除了分离逻辑中一个不合理的公理和其他冗余的推理规则，以表示系统的完备性。它引入了一个新的表达式，用于描述一个给定的状态在一个先决条件的完整信息。这项工作还使用了一个程序的必要和充分的先决条件，为中止自由执行，这使我们能够利用最强的后置条件。
This paper proves the completeness of an extension of Hoare's logic and separation logic for pointer programs with mutual recursive procedures. This paper shows the expressiveness of the assertion language as well. This paper achieves a new system by introducing two new inference rules, and removes an axiom that is unsound in separation logic and other redundant inference rules for showing completeness. It introduces a novel expression that is used to describe complete information of a given state in a precondition. This work also uses the necessary and sufficient precondition of a program for the abort-free execution, which enables us to utilize strongest postconditions.