Structural Operational Semantics

logic

Definition

Structural Operational Semantics

Structural Operational Semantics (also known as small-step semantics) describes the execution of a program as a sequence of individual computation steps. A single transition is typically written as:

$$⟨\Pi ,\sigma ⟩\to ⟨{\Pi }^{\prime },{\sigma }^{\prime }⟩$$

where $\Pi$ is the remaining program fragment to be executed, $\sigma \in \mathcal{S}$ is the current state, and the arrow $\to$ represents a single atomic transition to a new program ${\Pi }^{\prime }$ and state ${\sigma }^{\prime }$.

Small vs Big Step

Both structural operational semantics and natural semantics are operational semantics, since they model program execution as a sequence of computation steps.

Structural Operational Semantics

• close to the real machine model, since it represents individual computation steps
• captures low-level details such as interleaving, divergence, and program aborts
• useful when the execution path itself matters

Natural Semantics

• more abstract than SOS: it omits intermediate states and transition chains
• focuses on the final result of execution rather than the steps taken to reach it
• usually simpler to use because the definition is more compact

Examples

SIMPLE rules

The SOS of SIMPLE(ℤ) includes the following transition rules:

• Skip

  $$[\text{skip}]\sigma =\sigma$$

• Assignment

  $$[v:=e]\sigma ={\sigma }^{\prime }$$

  where

  $${\sigma }^{\prime }(w)=\{\begin{array}{ll}[e]\sigma & \text{if }w=v\\ \sigma (w)& \text{if }w\ne v\end{array}$$

• Sequencing

  $$[\Pi ;\Omega ]\sigma =[\Omega ]([\Pi ]\sigma )$$

• Conditional

  $$[\text{if }e\text{ then }\Pi \text{ else }\Omega \text{ fi}]\sigma =\{\begin{array}{ll}[\Pi ]\sigma & \text{if }[e]\sigma \ne 0\\ [\Omega ]\sigma & \text{if }[e]\sigma =0\end{array}$$

• While

  $$[\text{while }e\text{ do }\Pi \text{ od}]\sigma =\{\begin{array}{ll}[\text{while }e\text{ do }\Pi \text{ od}]([\Pi ]\sigma )& \text{if }[e]\sigma \ne 0\\ \sigma & \text{if }[e]\sigma =0\end{array}$$