Separation Logic for Non-local Control Flow and Block Scope Variables

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.