Syntax
We define our own imperative language and its syntax and semantics.
e::=x∣n∣e1+e2
c::=x:=eskipif e then c1 else c2while e do cc1;c2
Explanation:
eexpression - numbern, variable (identifier)x, addition of other expressions
ccommand - value assignment to variable, conditionals, sequential executionc1;c2
Semantics
= operational syntax
cprogram
μmemory
- under which
c
maps references to values
μ(e)returns value ofein memory
(c,μ)configuration
, provided by program after finishing (or just
μ
if finished) → see below
Update
Precondition:
x
is in memory
μ
.
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)=0Loop 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)=0Sequence
Different based on whether
c1
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′,μ′)