[[.: comm]]: Store -> Storebottom
[[L:=E: comm]](s) =
update([[L: intloc]], [[E: intexp]](s), s)
[[C_1;C_2: comm]](s) =
[[C_2: comm]]([[C_1:
comm]](s))
[[if E then C_1 else C_2 fi:
comm]](s) =
if([[E: boolexp]](s),
[[C_1: comm]](s), [[C_2:
comm]](s))
[[while E do C od: comm]](s) =
w(s)
where w(s) =
if([[E: boolexp]](s), w([[C:
comm]](s)), s)
[[skip: comm]](s) = s
The meaning of a command is a function from Store to Store.