Go backward to Non-Strict Command Execution Go up to Top Go forward to Retaining Multiple Stores

Example

begin
    X:=0;
    diverge;
    X:=2
return X+1

K[[begin X:=0; diverge; X:=2 return X+1]]s₀
= E[[X+1]] (C[[X:=0; diverge X:=2]]s₀)
= E[[X+1]] (C[[X:=2]](C[[diverge; X:=2]]s₀))

= E[[X+1]](C[[X:=2]]s₁)
= E[[X+1]](update [[X]] (E[[2]]s₁) s₁)
= E[[X+1]]([ [[X]] |-> (E[[2]]s₁) ]s₁)
= E[[X]]([ [[X]] |-> (E[[2]]s₁) ]s₁) plus one
= E[[2]]s₁ plus one
= two plus one
= three

s₁ = C[[X:=0; diverge]]s₀ needs not be simplified!