We present a semantic analysis of a recently proposed formalism for
local reasoning, where a specification (and hence proof) can
concentrate on only those cells that a program accesses. Our
main results are the soundness and, in a sense, completeness of
a rule that allows frame axioms, which describe invariant
properties of portions of heap memory, to be inferred automatically,
and thus avoided when writing specifications.