Natural Semantics

logic

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

Examples

SIMPLE rules

The natural semantics of SIMPLE(ℤ) can be given by the following 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}$$