Command Semantics

[[.: 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.