Go backward to Simplification Go up to Top Go forward to Program Denotation

Simplification

let s₁ = ( [ [[A]] |-> two] newstore)
    s₂ = [ [[Z]] |-> one ]s₁
    s' = C[[Z:=1; if A=0 then diverge; Z:=3]]s₁
    in access [[Z]] s'
= let s₁ = ( [ [[A]] |-> two] newstore)
    s₂ = [ [[Z]] |-> one ]s₁
    s' = [ [[Z]] |-> three ]s₂
    in access [[Z]] s'

access [[Z]] s'
= access [[Z]] [ [[Z]] |-> three ]s₂
= [ [[Z]] |-> three ]s₂ [[Z]]
= three