Structural Operational Semantic

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

Characteristics

• Granularity: SOS provides the finest level of detail, making it suitable for reasoning about interleaving and concurrency.
• Non-termination: Infinite loops are explicitly represented as infinite transition chains $⟨\Pi ,\sigma ⟩\to ⟨{\Pi }^{\prime },{\sigma }^{\prime }⟩\to \dots$.
• Termination: A terminal state is reached when the program component is empty (e.g., $⟨\text{skip},\sigma ⟩$).