Abstract
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.
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.
Originalsprog | Engelsk |
---|---|
Titel | Foundations of Software Science and Computational Structures : 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings |
Redaktører | Martin Hofman |
Antal sider | 15 |
Forlag | Springer |
Publikationsdato | 2011 |
Sider | 305-319 |
ISBN (Trykt) | 978-3-642-19804-5 |
ISBN (Elektronisk) | 978-3-642-19805-2 |
DOI | |
Status | Udgivet - 2011 |
Begivenhed | 14th International Conference on Foundations of Software Science and Computational Structures - Saarbrücken, Tyskland Varighed: 26 mar. 2011 → 3 apr. 2011 Konferencens nummer: 14 |
Konference
Konference | 14th International Conference on Foundations of Software Science and Computational Structures |
---|---|
Nummer | 14 |
Land/Område | Tyskland |
By | Saarbrücken |
Periode | 26/03/2011 → 03/04/2011 |
Navn | Lecture notes in computer science |
---|---|
Vol/bind | 6604 |
ISSN | 0302-9743 |