Publication details

Saarland University Computer Science

A Step-indexed Kripke Model of Hidden State

Jan Schwinghammer, Lars Birkedal, Franšois Pottier, Bernhard Reus, Kristian St°vring, Hongseok Yang

Mathematical Structures in Computer Science, 2012

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.

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009