Go backward to Example Go up to Top Go forward to Non-Strict Command Execution

Example

s₂ = update [[Y]] (E[[X+1]]s₁) s₁
s₃ = update [[X]] (E[[4]]s₂) s₂

E[[Y]] (C[[Y:= X+1; X:=4]] s₁)
= E[[Y]]s₃
= access [[Y]] s₃
= E[[X+1]]s₁
= E[[X]]s₁ plus one
= (access [[X]] s₁) plus one
= E[[0]]s₀ plus one
= zero plus one
= one

• Evaluation E[[X]]s₁ required.
• Old store s₁ must be retained.
• E[[X]]s₃ would be five!