3. Big-Step Semantics

Evaluation Sequence

We will classify evaluation sequences in three categories:

• Terminating: if the sequence eventually reaches a terminal non-blocked configuration, i.e. $⟨n,s⟩$ where $n$ is integer, $⟨b,s⟩$ where $b$ is boolean, or $⟨skip,s⟩$. e.g. $⟨\text{if }4=0\text{ then }skip\text{ else }skip,s⟩$
• Blocked: if the sequence eventually reaches a blocked configuration, i.e. $⟨!I,s⟩$ where $I\notin \text{dom}(s)$. e.g. $⟨\text{if }!x=0\text{ then }skip\text{ else }skip,s⟩$ is stuck if $\text{dom}(s)$ does not contain $x$
• Divergent: if the sequence is infinite. e.g. $⟨\text{while True do }skip,s⟩$

Big-Step Semantics

Big-Step Semantics

The goal is to define a binary relation between configurations, which associates a configuration with its corresponding terminal one if it exists. That is, define by induction the binary relation $⟨P,s⟩{\to }^{\ast }⟨P^{\prime },s^{\prime }⟩$ such that $⟨P^{\prime },s^{\prime }⟩$ is terminal.

The usual notation for this is $⟨P,s⟩\Downarrow ⟨P^{\prime },s^{\prime }⟩$. In other words: $⟨P,s⟩\Downarrow ⟨P^{\prime },s^{\prime }⟩\text{ if }⟨P,s⟩{\to }^{\ast }⟨P^{\prime },s^{\prime }⟩$ where $⟨P^{\prime },s^{\prime }⟩$ is terminal.

Link to original

Big-Step Semantics for SIMP

Below are all the big-step semantics required for SIMP.

Example Proof

Consider the program $P:(z:=!x;x:=!y);y:=!z$ and a state $s$ such that:

• $s(z)=0$
• $s(x)=1$
• $s(y)=2$

We can prove that $P\Downarrow ⟨skip,s^{\prime }⟩$ where $s^{\prime }$ is a state such that:

• $s^{\prime }(z)=1$
• $s^{\prime }(x)=2$
• $s^{\prime }(y)=1$

First notice that:

$$\frac{\frac{\overline{⟨!x,s⟩\Downarrow ⟨1,s⟩}}{⟨z:=!x,s⟩\Downarrow ⟨skip,s[z\mapsto 1]⟩}\frac{\overline{⟨!y,s[z\mapsto 1]⟩\Downarrow ⟨2,s[z\mapsto 1]⟩}}{⟨x:=!y,s[z\mapsto 1]⟩\Downarrow ⟨skip,s\left[\begin{array}{c}z\mapsto 1\\ x\mapsto 2\end{array}\right]⟩}}{⟨z:=!x;x:=!y,s⟩\Downarrow ⟨skip,s\left[\begin{array}{c}z\mapsto 1\\ x\mapsto 2\end{array}\right]⟩}$$

Using this we can prove: $$\large \frac{ {\large \left< z := !x; x:= !y, s \right> \Downarrow \left< skip, s \begin{bmatrix} z \mapsto 1 \ x \mapsto 2 \end{bmatrix} \right>}

\frac{
	\overline{
		\left< !z, s \begin{bmatrix} z \mapsto 1 \\ x \mapsto 2 \end{bmatrix} \right> \Downarrow \left< 1, s \begin{bmatrix} z \mapsto 1 \\ x \mapsto 2 \end{bmatrix} \right>
	}
}{
	\left< y:= !z, s \begin{bmatrix} z \mapsto 1 \\ x \mapsto 2 \end{bmatrix} \right> \Downarrow \left< skip, s \begin{bmatrix} z \mapsto 1 \\ x \mapsto 2 \\ y \mapsto 1 \end{bmatrix} \right>
}

}{ \large \left< P,s \right> \Downarrow \left< skip, s’ \right> }$$

Adding Variable Declarations

We want to introduce the syntax: $C::=\text{begin loc }x:=E;C\text{ end}$ We add the following big-step semantics rule:

$$\frac{⟨E,s⟩\Downarrow ⟨n,s^{\prime }⟩⟨C\{x\mapsto I\},s^{\prime }[I\mapsto n]⟩\Downarrow ⟨skip,s^{\prime \prime }[I\mapsto n^{\prime }]⟩}{⟨\text{begin loc }x:=E;C\text{ end},s⟩\Downarrow ⟨skip,s^{\prime \prime }⟩}$$

Where $I\notin \text{dom}(s^{\prime })\cup \text{dom}(s^{\prime \prime })\cup \text{locations}(C)$, that is $I$ is a fresh name. Where $C\{x\mapsto I\}$ is the program $C$ where all occurrences of $x$ are replaced by $I$.

Example: swap two variables $x,y$ using local variable $z$

begin
	loc z := !x;
	x := !y;
	y != z
end

To show program $P$ is correct, we first prove: $⟨x:=!y,y:=!I,s[I\mapsto s(x)]⟩\Downarrow ⟨skip,s[x\mapsto s(y),y\mapsto s(x)]⟩$ (refer to previous examples)

Let $s^{\prime }$ be the store $s[x\mapsto s(y),y\mapsto s(x)]$, then: $\frac{\overline{⟨!x,s⟩\Downarrow ⟨s(x),s⟩}⟨x:=!y;y:=!I,s[I\mapsto s(x)]⟩\Downarrow ⟨skip,s^{\prime }⟩}{⟨P,s⟩\Downarrow ⟨skip,s^{\prime }⟩}$