IV. Valuation functions:
C: Command -> Store -> Answer
C[[C_1; C_2]]s = (C[[C_1]] then
C[[C_2]])s
C[[I := E]]s = (true, update [[I]] (E[[E]]s) s)
C[[if G fi]]s = T[[G]]s ->
G[[G]]s [] (false, s)
C[[do G od]]s =
T[[G]]s -> (G[[G]] then C[[do G
do]])(s) [] (true, s)
T: Guarded-command -> Store -> Tr
T[[G_1 [] G_2]]s = (T[[G_1]]s) or
(T[[G_2]]s)
T[[B -> C]]s = B[[B]]s
G: Guarded-command -> Store ->
Answer
G[[G_1 [] G_2]]s = (G[[G_1]]s) join
(G[[G_2]]s)
G[[B -> C]]s = B[[B]]s ->
C[[C]]s [] no-answer
E:Expression -> Store -> Nat
B:Boolean-expr -> Store -> Tr