Abstract
Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context. We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Charguéraud 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 generalised frame and anti-frame rules, where invariants are generalised to families of invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.
| Original language | English |
|---|---|
| Journal | Mathematical Structures in Computer Science |
| Volume | 23 |
| Issue number | 1 |
| Pages (from-to) | 1-54 |
| Number of pages | 54 |
| ISSN | 0960-1295 |
| DOIs | |
| Publication status | Published - Feb 2013 |