Go backward to Valuation Functions Go up to Top Go forward to Error Handling

Composition of States

C[[C₁; C₂]] = C[[C₁]] check-cmd C[[C₂]]

Command = State -> Post-state_{_|_}
check-cmd: Command × Command -> Command
h₁ check-cmd h₂ =
    lambda a. let z = h₁(a) in
    cases z of
        isOK(s, i, o) -> h₂(s, i, o)
        isErr(s, i, o) -> z
    end

1. Give current state a to C[[C₁]] producing a post-state z = C[[C₂]]a'.
2. If z is a proper state a' and if the state component is OK, produce C[[C₂]]a'
3. If z is errnoneous, C[[C₂]] is ignored and z is the result.

Similar for check of expression results.