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 }$.