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 discuss the semantic foundations of frame and anti-frame rules, and
present the first sound model for Chargueraud and Pottier's
type and capability system including both of these rules.
The model is a possible worlds model
based on the operational semantics and step-indexed heap relations,
and the worlds are given by 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 preorders.
This generalization enables reasoning about some well-bracketed as well as
(locally) monotone uses of local state.