Go backward to Non-strict Store Updates Go up to Top Go forward to Example

Example

begin
     X := 0
     Y := X+1
     X := 4
return Y

K: Block -> Store_{_|_} -> Nat_{_|_}
K[[begin C return E]] =
    lambda s. E[[E]] (C[[C]]s)

K[[begin X:=0; Y:= X+1; X:=4 return Y]]s₀
= E[[Y]] (C[[X:=0; Y:= X+1; X:=4]]s₀)
= E[[Y]] (C[[Y:= X+1; X:=4]] (C[[X:=0]]s₀))
= E[[Y]] (C[[Y:= X+1; X:=4]]
    (update [[X]] (E[[0]]s₀) s₀))
= E[[Y]] (C[[Y:= X+1; X:=4]] s₁)

s₁ = (E[[0]]s₀) needs not be simplified!