Valuation Functions

P: Program -> Store -> P(Store)
P[[C]] = flatten(C[[C]])

C: Command -> Res
C[[I := E]] = step(lambda(s). update [[I]] (E[[E]]s) s)
C[[C_1; C_2]] = C[[C_1]] seq C[[C_2]]
C[[C_1 || C_2]] = C[[C_1]] par C[[C_2]]
C[[if B then C_1 else C_2]](s) = B[[B]]s ->
    (pause (C[[C_1]]) s) []
    (pause (C[[C_2]]) s)
C[[while B do C]](s) = B[[B]]s ->
    (pause (C[[C]] seq C[[while B do C]]) s) []
    (step (lambda(s). s) s)