Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1017/S0960129512000035 | Mathematical Structures in Computer Science |
Keywords | Field | DocType |
step-indexed kripke model,sound model,irrelevant part,possible worlds model,metric space,capability system,frame rule,modular reasoning,local state,generalised frame,hidden state,anti-frame rule | Discrete mathematics,Operational semantics,Generalization,Heap (data structure),Invariant (mathematics),Metric space,Monotone polygon,Recursion,Mathematics,Possible world | Journal |
Volume | Issue | ISSN |
23 | 1 | 0960-1295 |
Citations | PageRank | References |
1 | 0.36 | 20 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jan Schwinghammer | 1 | 166 | 13.60 |
| Lars Birkedal | 2 | 1481 | 96.84 |
| François Pottier | 3 | 389 | 29.68 |
| Bernhard Reus | 4 | 276 | 27.17 |
| Kristian Støvring | 5 | 64 | 6.91 |
| Hongseok Yang | 6 | 2313 | 115.85 |