Simple imperative language

Syntax

We define our own imperative language and its syntax and semantics.

$e \quad::= \quad x ~ |~n~ |~ e_{1}+e_{2}$

$c \quad::= \quad x:=e \\\qquad\qquad~ \text{skip} \\\qquad\qquad~ \text{if } e \text{ then } c_1 \text{ else } c_2 \\\qquad\qquad~ \text{while } e \text{ do } c \\\qquad\qquad~ c_1;c_2$

Explanation:

$e$ expression - number $n$ , variable (identifier) $x$ , addition of other expressions

$c$ command - value assignment to variable, conditionals, sequential execution $c_1;c_2$

Semantics

= operational syntax

$c$ program

$\mu$ memory - under which $c$ maps references to values

$\mu(e)$ returns value of $e$ in memory

$(c,\mu)$ configuration , provided by program after finishing (or just $\mu$ if finished) → see below

Update

Precondition: $x$ is in memory $\mu$ .

x∈dom⁡(μ)(x:=e,μ)→μ[x↦μ(e)]\frac{x \in \operatorname{dom}(\mu)}{(x:=e, \mu) \rightarrow \mu[x \mapsto \mu(e)]}(x:=e,μ)→μ[x↦μ(e)]x∈dom(μ)

No-Op

(skip,μ)→μ(\text { skip, } \mu) \rightarrow \mu(skip,μ)→μ

Branch True / False

μ(e)≠0(ifethenc1elsec2,μ)→(c1,μ)\frac{\mu(e) \neq 0}{\left(\text {if } e \text { then } c_{1} \text { else } c_{2}, \mu\right) \rightarrow\left(c_{1}, \mu\right)}(ifethenc1elsec2,μ)→(c1,μ)μ(e)=0

μ(e)=0(ifethenc1elsec2,μ)→(c2,μ)\frac{\mu(e)=0}{\left(\text { if } e \text { then } c_{1} \text { else } c_{2}, \mu\right) \rightarrow\left(c_{2}, \mu\right)}(ifethenc1elsec2,μ)→(c2,μ)μ(e)=0

Loop True / False

μ(e)≠0(whileedoc,μ)→(c;whileedoc,μ)\frac{\mu(e) \neq 0}{(\text {while } e \text { do } c, \mu) \rightarrow(c ; \text { while } e \text { do } c, \mu)}(whileedoc,μ)→(c;whileedoc,μ)μ(e)=0

μ(e)=0(whileedoc,μ)→μ\frac{\mu(e)=0}{(\text {while } e \text { do } c, \mu) \rightarrow \mu}(whileedoc,μ)→μμ(e)=0

Sequence

Different based on whether $c_1$ calls other instructions or not.

(c1,μ)→μ′(c1;c2,μ)→(c2,μ′)\frac{\left(c_{1}, \mu\right) \rightarrow \mu^{\prime}}{\left(c_{1} ; c_{2}, \mu\right) \rightarrow\left(c_{2}, \mu^{\prime}\right)}(c1;c2,μ)→(c2,μ′)(c1,μ)→μ′

(c1,μ)→(c1′,μ′)(c1;c2,μ)→(c1′;c2,μ′)\frac{\left(c_{1}, \mu\right) \rightarrow\left(c_{1}^{\prime}, \mu^{\prime}\right)}{\left(c_{1} ; c_{2}, \mu\right) \rightarrow\left(c_{1}^{\prime} ; c_{2}, \mu^{\prime}\right)}(c1;c2,μ)→(c1′;c2,μ′)(c1,μ)→(c1′,μ′)