Structural operational semantics through context-dependent behaviour

We present a new approach to providing a structural operational semantics for imperative programming languages with concurrency and procedures. The approach is novel because we expose the building block operations—variable assignment and condition checking—in the labels on the transitions; these form the context-dependent behaviour of a program. Using this style results in two main advantages over standard formalisms for imperative programming language semantics: firstly, our individual transition rules are more concise, and secondly, we are able to more abstractly and intuitively describe the semantics of procedures, including by-value and by-reference parameters. Standard techniques in the literature tend to result in complex and hard-to-read rules for even simple language constructs when procedures and parameters are dealt with. Our semantics for procedures utilises the context-dependent behaviour in the transition label to handle variable name scoping, and defines the semantics of recursion without requiring additional rules. In contrast with Plotkin’s seminal structural operational semantics paper, we do not use locations to describe some of the more complex language constructs. Novel aspects of the abstract syntax include local states (in contrast to a single global store), which simplifies the reasoning about local variables, and a command for dynamically renaming variables (in contrast to mapping variables to locations), which simplifies the reasoning about the effect of procedures on by-reference parameters.

► We present a novel style of operational semantics for imperative languages.
► We formalise concurrency, procedures, recursion and functions with side-effects.
► The provide both big-step and small-step versions of the rules.
► The semantics does not require locations, and is modular