Frame and anti-frame rules have been proposed as proof rules for
modular reasoning about programs. Frame rules allow one to hide
irrelevant parts of the state during verification, whereas the
anti-frame rule allows one to hide local state from the context. We
give the first sound model for Chargu\'eraud and Pottier's
type and capability system including both frame and anti-frame rules.
The model is a possible worlds model
based on the operational semantics and step-indexed heap relations, and
the worlds are constructed as a recursively defined predicate on a
recursively defined metric space.
We also extend the model to account for Pottier's generalized frame and anti-frame rules, where
invariants are generalized to families of invariants
indexed over pre-orders. This generalization enables reasoning about some
well-bracketed as well as (locally) monotonic uses of local state.
A preliminary version of this article (not including the generalized frame and anti-frame rules) has been presented at the 7th Workshop on Fixed Points in Computer Science, FICS 2010.