Publication details

Saarland University Computer Science

A Step-indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces

Jan Schwinghammer, Lars Birkedal, Kristian StÝvring

Foundations of Software Science and Computation Structures (FOSSACS'11), Springer, March 2011

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.

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009