previous up next
Go backward to Semantic Algebras
Go up to Top
Go forward to Expression Semantics
RISC-Linz logo

Command Semantics

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

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

Author: Wolfgang Schreiner
Last Modification: March 26, 1998

previous up next