A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces
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éraud 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.
- 1.Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: POPL (2009)Google Scholar
- 5.Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. LMCS 2(5:1) (2006)Google Scholar
- 6.Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL (to appear, 2011)Google Scholar
- 8.Charguéraud, A., Pottier, F.: Functional translation of a calculus of capabilities. In: Proceedings of ICFP, pp. 213–224 (2008)Google Scholar
- 9.Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Proceedings of POPL, pp. 262–275 (1999)Google Scholar
- 10.Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. In: Proceedings of ICFP (2010)Google Scholar
- 12.Pilkiewicz, A., Pottier, F.: The essence of monotonic state (July 2010) (unpublished)Google Scholar
- 14.Pottier, F.: Hiding local state in direct style: a higher-order anti-frame rule. In: Proceedings of LICS, pp. 331–340 (2008)Google Scholar
- 15.Pottier, F.: Generalizing the higher-order frame and anti-frame rules (July 2009) (unpublished), http://gallium.inria.fr/~fpottier
- 18.Smyth, M.B.: Topology. In: Handbook of Logic in Computer Science, vol. 1. Oxford Univ. Press, Oxford (1992)Google Scholar