Operational Semantics
Operational semantics is an alternative style of semantics that emphasises the steps taken during the execution of the program. We will construct an operational semantics for While programs (our toy imperative language) by building on the denotational semantics for arithmetic and Boolean expressions.
The statements of the While language are defined as follows.
A statement is an element of the following grammar:
\[S \Coloneqq \mathsf{skip} \mid x \leftarrow A \mid S; S \mid \mathsf{if}\ B\ \{ S \}\ \mathsf{else}\ \{ S \} \mid \mathsf{while}\ B\ \{ S \}\]where $A$ stands for any arithmetic expression and $B$ stands for any Boolean expression.
As with the denotational semantics for expressions, we will work with the abstract syntax tree of statement rather than the string that produced them, using $\mathcal{S}$ to refer to the set of statements.
The specific type of operational semantics that we will use is called big-step or “natural” semantics. Big-step semantics describes the overall effect of executing a statement, relating an initial state directly to the final state produced.
The big-step judgement $\langle S,\, \sigma_1 \rangle \Downarrow \sigma_2$ says “the statement $S$ executed from the state $\sigma_1$ terminates with the final state $\sigma_2$”.
Formally, ${\Downarrow} \subseteq \mathcal{S} \times \mathsf{State} \times \mathsf{State}$, i.e. it is a ternary relation between statements, initial states, and final states, with $(S,\, \sigma_1,\, \sigma_2) \in {\Downarrow}$ being written $\langle S,\, \sigma_1 \rangle \Downarrow \sigma_2$.
We shall define this relation by a series of inference rules.
Skip
\[\dfrac {} {\langle \mathsf{skip},\, \sigma \rangle \Downarrow \sigma}\]The fraction-esque notation denotes an inference rule. Above the line is a series of premises which we must show in order to use the rule, and below the line is the conclusion - you can read it as “if everything above the line holds, then everything below the line holds.” Such inference rules are a common way of inductively defining a relation. Formally, the relation is defined as the least relation satisfying these inference rules.
In the case of the $\mathsf{skip}$ command it says: when executing this program from an initial state $\sigma$, then final state will also be $\sigma$. For instance, we have that $\langle \mathsf{skip},\, [x \mapsto 4] \rangle \Downarrow [x \mapsto 4]$.
Within these rules there are metavariables such as $\sigma$ that are act as parameters to the rule can be instantiated as required; in other words, the rule is universally quantified by such variables. Note they are referred to as metavariables rather than simply variables to distinguish them from the program’s variables.
Assignment
Intuitively, when the assignment statement $x \leftarrow e$ is executed with a given state $\sigma$, the value of the arithmetic expression $e$ is calculated in this state using its denotation function, and the state is updated so that $x$ is mapped to this value. Corresponding, the inference rule for describing the behaviour of the assignment state is as follows:
\[\dfrac {} {\langle x \leftarrow e,\, \sigma \rangle \Downarrow \sigma[x \mapsto \llbracket e \rrbracket_A(\sigma)]}\]The notation $\sigma[x \mapsto n]$ refers to the state that results from updating the value assigned to $x$ to be $n$. Note that it will be evaluated under the previous state, not the newly derived state. The evaluation of the arithmetic expression doesn’t constitute an execution step in its own right - our operational semantics only cares about the evolution of statements.
For example, the rule tell us that $\langle x \leftarrow x + 1,\, [x \mapsto 2] \rangle \rightarrow [x \mapsto 3]$ where we have instantiated the rule with the variable $x$, the arithmetic expression $x + 1$, and the state $[x \mapsto 2]$. The state $[x \mapsto 3]$ is determined as $[x \mapsto 2]$ updated such that $x \mapsto \llbracket x + 1 \rrbracket_\mathcal{A}([x \mapsto 2])$; hence, $[x \mapsto 3]$. As with the $\mathsf{skip}$ statement, this rule doesn’t require any premises as it’s behaviour be described without making reference to other statements as it is not a compound statement (i.e. it is a base case of the grammar).
Sequence
The next rule we will look at are those governing the operational semantics of the sequence construct $S_1;\; S_2$.
Intuitively, such a program proceed by first executing $S_1$ and then subsequently executing $S_2$. We encode this behaviour using a condition inference rule, i.e. one with premises:
\[\dfrac {\langle S_1,\, \sigma_1 \rangle \Downarrow \sigma_2\ \langle S_2,\, \sigma_2 \rangle \Downarrow \sigma_3} {\langle S_1;\; S_2,\, \sigma \rangle \Downarrow \sigma_3}\]That is, if we know that executing $S_1$ in the state $\sigma_1$ leads to $\sigma_2$, and executing $S_2$ in the state $\sigma_2$ leads to $\sigma_3$, then we can conclude that executing $S_1;\; S_2$ in the state $\sigma_1$ will lead to $\sigma_3$.
As with the previous rules, this rule apply for all statements $S_1,\, S_2 \in S$ and all states $\sigma_1,\, \sigma_2,\, \sigma_3 \in \mathsf{State}$ - these are the rules metavariables. In order to use this rule, however, we need not only to instantiate metavariables but also the premises by determining the behaviour of the statements $S_1$ and $S_2$.
For example, we know that $\langle x \leftarrow 2,\, [x \mapsto 1] \rangle \Downarrow [x \mapsto 2]$ by the assignment rule and $\langle x \leftarrow x * 2,\, [x \mapsto 2] \rangle \Downarrow [x \mapsto 4]$. Therefore, we can conclude: \(\langle x \leftarrow 2; x \leftarrow x * 2,\, [x \mapsto 1] \rangle \Downarrow [x \mapsto 4]\).