We present an approach for handling non-local control flow (goto and return statements) in the presence of allocation and deallocation of block scope variables in imperative programming languages. We define a small step operational semantics and an axiomatic semantics (in the form of a separation logic) for a small C-like language that combines these two features, and which also supports pointers to block scope variables. Our operational semantics represents the program state through a generalization of Huet's zipper data structure. We prove soundness of our axiomatic semantics with respect to our operational semantics. This proof has been fully formalized in Coq. © 2013 Springer-Verlag.
CITATION STYLE
Krebbers, R., & Wiedijk, F. (2013). Separation logic for non-local control flow and block scope variables. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7794 LNCS, pp. 257–272). https://doi.org/10.1007/978-3-642-37075-5_17
Mendeley helps you to discover research relevant for your work.