Structural operational semantics through context-dependent behaviour

We present an operational semantics for an imperative language 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 existing formalisms for imperative programming language semantics: firstly, our individual transition rules are less cluttered, and secondly, we are able to more abstractly and intuitively describe the semantics of procedures, including by-value and by-reference parameters. Existing techniques in the literature tend to result in complex and hard-to-read rules for even simple language constructs, or avoid discussion of procedures and parameters entirely. Our semantics for procedures utilises the context-dependent behaviour in the transition label to neatly handle variable name scoping, and defines the semantics of recursion without requiring additional rules. We also demonstrate how the semantics may be extended to handle function calls within expressions, array element and record field updates, and higher-order programming constructs