论文标题
魔术棒的声音自动化（扩展版）
Sound Automation of Magic Wands (extended version)
论文作者
论文摘要
Magic Wand $ \ Mathbin { - \！\！*} $（也称为分离含义）是一种分离逻辑连接，通常用于指定部分数据结构的属性，例如在迭代遍历期间。 Magic Wand Formula $ a \ Mathbin { - \！\！*} B $的足迹是一种状态，结合$ a $保留的任何状态，产生了$ b $持有的状态。证明魔术魔杖（也称为包装魔杖）的主要挑战是找到这样的足迹。现有的软件包算法要么具有较高的注释开销，要么正如我们在本文中所显示的那样，这是不合适的。我们提出了一个正式的框架，该框架精确地描述了适用于大型分离逻辑的可能包装算法的广泛设计空间。我们在Isabelle/Hol中证明我们的正式框架是合理而完整的，并使用它来开发一种具有竞争性自动化和合理性的新颖包装算法。此外，我们提出了魔杖的新颖，有限的定义，并在伊莎贝尔/hol中证明了可以很好地结合这种魔杖的分数，而任意魔杖并非如此。我们已经为毒蛇语言实施了我们的技术，并证明它们在实践中是有效的。
The magic wand $\mathbin{-\!\!*}$ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula $A \mathbin{-\!\!*} B$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds. The key challenge of proving a magic wand (also called packaging a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or, as we show in this paper, are unsound. We present a formal framework that precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics. We prove in Isabelle/HOL that our formal framework is sound and complete, and use it to develop a novel package algorithm that offers competitive automation and is sound. Moreover, we present a novel, restricted definition of wands and prove in Isabelle/HOL that it is possible to soundly combine fractions of such wands, which is not the case for arbitrary wands. We have implemented our techniques for the Viper language, and demonstrate that they are effective in practice.
