Operational Semantic

logic verification programming-languages

Definition

Operational Semantics

Operational semantics describe the meaning of a program by specifying how it executes on an abstract machine. It defines the transitions between states of the computation.

Types

Structural Operational Semantics (SOS)

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

Link to original

Natural Semantics

Definition

Natural Semantics

Natural semantics (also known as big-step semantics) describes the overall result of executing a statement in its entirety, rather than the individual steps. A transition is written as:

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

This indicates that executing the program fragment $\Pi$ starting in state $\sigma \in \mathcal{S}$ results in the final state ${\sigma }^{\prime }\in \mathcal{S}$.

Link to original

Comparison

Feature	Small-step (SOS)	Big-step (Natural)
Granularity	Detailed (individual steps)	Abstract (final result)
Non-termination	Explicitly represented by infinite chains	Cannot easily distinguish from divergence
Complexity	Higher (requires tracking intermediate states)	Lower (more direct)

Relation to Hoare Calculus

The Hoare calculus provides an axiomatic semantics, which abstracts away from the specific execution steps defined by operational semantics and focuses instead on assertions about the state.