  Separation logic adds two connectives to assertion languages: separating
conjunction * ("star") and its adjoint, separating implication -* ("magic
wand"). Comparatively, separating implication is less widely used.
  This paper demonstrates that by using magic wand to express frames that
relate mutable local portions of data structures to global portions, we can
exploit its power while proofs are still easily understandable. Many useful
separation logic theorems about partial data structures can now be proved by
simple automated tactics, which were usually proved by induction. This
magic-wand-as-frame technique is especially useful when formalizing the proofs
by a high order logic. We verify binary search tree insert in Coq as an example
to demonstrate this proof technique.
