### Abstract

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 are unsound. In this entry, we formally define a framework for the sound automation of magic wands, described in an upcoming paper at CAV 2022, and prove that it is sound and complete. This framework, called the package logic, precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Session Package_logic

- SepAlgebra
- PackageLogic

### Used by

- A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand

## Cite

×

Package_logic-AFP

    @article{Package_logic-AFP,
      author  = {Thibault Dardinier},
      title   = {Formalization of a Framework for the Sound Automation of Magic Wands},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Package_logic.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- May 27, 2022 : Isabelle2021-1