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.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten