A Step-Indexed Kripke Model of Hidden State

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 113
  • Download : 0
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 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 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.
Publisher
CAMBRIDGE UNIV PRESS
Issue Date
2013-02
Language
English
Article Type
Article
Citation

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, v.23, no.1, pp.1 - 54

ISSN
0960-1295
DOI
10.1017/S0960129512000035
URI
http://hdl.handle.net/10203/225275
Appears in Collection
CS-Journal Papers(저널논문)
Files in This Item
There are no files associated with this item.

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0