Go backward to Semantic Algebras Go up to Top Go forward to Expression Semantics

Command Semantics

[[.: comm]]: Store -> Storebottom

[[L:=E: comm]](s) =
    update([[L: intloc]], [[E: intexp]](s), s)
[[C₁;C₂: comm]](s) =
    [[C₂: comm]]([[C₁: comm]](s))
[[if E then C₁ else C₂ fi: comm]](s) =
    if([[E: boolexp]](s),
        [[C₁: comm]](s), [[C₂: 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.