Rule-Based Operational Semantics for an Imperative Language

Operational semantics for programming languages usually come in two flavours: big-step and small-step. Both are defined using deduction rules with a congruence rule allowing reduction in certain contexts. For a description based on rewrite rules, known approaches consist in deriving an abstract machine, which is very close to implementation. In this paper, we describe the operational semantics of an imperative language in a rule-based style, arguably as abstract as the other kinds of semantics. Moreover, we combine the approach with the store-based semantics, which puts the focus on memory states rather than values, which is more appropriate for imperative languages.