2. Small-Step Semantics

Small-Step Semantics

We define a transition system with configurations $⟨P,s⟩$ where $P$ is a program (for example a SIMP program) and $s$ is a store (memory) represented by a partial function from locations to integers.

Notation: $s[I\mapsto n]$ denotes the function $s^{\prime }$ that coincides with $s$ except that it associated to $I$ the value $n$, more precisely:

• $s[I\mapsto n](I)=n$
• $s[I\mapsto n](I^{\prime })=s(I^{\prime })\text{ if }I\ne I^{\prime }$

The transition relation -> on configurations is inductively defined by the axioms and rules:

• the expression $E$ has the value $n$ in the memory state $s$ if $⟨E,s⟩{\to }^{\ast }⟨n,s^{\prime }⟩$
• the command $C$ has a successful execution in the memory state $s$ if $⟨C,s⟩{\to }^{\ast }⟨skip,s^{\prime }⟩$ . We say that $C$ in $s$ produces $s^{\prime }$.

Link to original

Small-Step Semantics for Expressions

Below are the definitions for SIMP expressions using small-step semantics.

Example: Let $s$ be a state such that $s(z)=0$ and let $E=!z+1$. The expression $E$ evaluates to $1$ in $s$, since $⟨!z+1,s⟩\to ⟨0+1,s⟩\to ⟨1,s⟩$ This is shown as follows: $\begin{array}{r}1.\frac{\frac{}{}()}{⟨!z+1,s⟩\to ⟨0+1,s⟩}({\text{op}}_L)\end{array}$

Small-Step Semantics for Commands

Below are the definitions for SIMP commands using small-step semantics.

Example: Let $P$ be the program $z:=!x;x:=!y;y:=!z$ and $s$ (a state such that $s(z)=0,s(x)=1,s(y)=2$). There is a sequence of transitions:

Remarks

There are no axiom or rules for programs of the form:

• $⟨n,s⟩$ where $n$ is an integer
• $⟨b,s⟩$ where $b$ is a boolean
• $⟨!I,s⟩$ where $I\notin dom(s)$
• $⟨skip,s⟩$

These are terminal configurations. In the case of $⟨!I,s⟩$ where $I\notin dom(s)$ we say that the program is blocked.

Compared with the abstract machine:

1. Each transition here is doing a part of the computation that leads to the result, whereas some of the transitions of the machine were only manipulating syntax.
2. Though to show a sequence of reductions is valid, we need a proof.

Determinism

Small-step semantics are deterministic. Given a configuration $⟨P,s⟩$ there is a unique sequence of transitions from $⟨P,s⟩$ with maximal length. This is called the evaluation sequence for $⟨P,s⟩$. It may be finite.