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 ing an abstract machine, which is very close to implementation. In this paper, we describe the operational semantics of an imperative 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.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Florent Kirchner, François-Régis Sinot
• Keywords: Certain Contexts, Congruence Rule, ENTCS 2007, Operational Semantics