Witnessing the elimination of magic wands.
Witnessing the elimination of magic wands.
复制标题
目睹消除魔术棒。
DOI：
10.1007/s10009-015-0372-3
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Huisman M
中科院分区：
文献类型：
--
作者：
Blom S;Huisman M
本文讨论了静态验证的程序，已指定使用分离逻辑与魔杖。魔棒用于指定分离逻辑中的不完整资源，即，如果提供了缺失的资源，则可以使用魔杖将其交换为已完成的资源。魔术棒操作符的应用之一是描述遍历数据结构的算法的循环不变量，例如树删除问题的命令式版本（来自VerifyThis@FM2012程序验证竞赛的挑战3），这是我们工作的激励示例。大多数基于分离逻辑的静态验证工具不支持魔杖，可能是因为包含魔杖的公式的有效性本身是不可判定的。为了避免这个问题，在我们的方法中，程序注释器必须为魔杖提供一个见证，从而避免由于使用魔杖而导致的不可判定性。见证服务器是一个对象，它对魔杖指定的权限交换指令和交换过程中所需的额外资源进行编码。我们将展示如何使用此见证信息来编码一个规范与魔杖作为一个规范没有魔杖。具体地说，这种方法被用在VerCors工具集中：带注释的Java程序被编码为Chalice程序。然后，Chalice进一步将程序翻译为BoogiePL，在那里生成适当的证明义务。除了我们的编码的魔杖，我们还讨论了其他方面的注释到圣杯的Java程序的编码，特别是，编码的抽象谓词与权限参数。我们说明了我们的方法上的树删除算法，并验证一个链表的迭代器。
This paper discusses static verification of programs that have been specified using separation logic with magic wands. Magic wands are used to specify incomplete resources in separation logic, i.e., if missing resources are provided, a magic wand allows one to exchange these for the completed resources. One of the applications of the magic wand operator is to describe loop invariants for algorithms that traverse a data structure, such as the imperative version of the tree delete problem (Challenge 3 from the VerifyThis@FM2012 Program Verification Competition), which is the motivating example for our work. Most separation logic-based static verification tools do not provide support for magic wands, possibly because validity of formulas containing the magic wand is, by itself, undecidable. To avoid this problem, in our approach the program annotator has to provide a witness for the magic wand, thus circumventing undecidability due to the use of magic wands. A witness is an object that encodes both instructions for the permission exchange that is specified by the magic wand and the extra resources needed during that exchange. We show how this witness information is used to encode a specification with magic wands as a specification without magic wands. Concretely, this approach is used in the VerCors tool set: annotated Java programs are encoded as Chalice programs. Chalice then further translates the program to BoogiePL, where appropriate proof obligations are generated. Besides our encoding of magic wands, we also discuss the encoding of other aspects of annotated Java programs into Chalice, and in particular, the encoding of abstract predicates with permission parameters. We illustrate our approach on the tree delete algorithm, and on the verification of an iterator of a linked list.