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

Simplification II

P[[Z:=1; if A=0 then diverge; Z:=3.]](zero)
= let s₃ = [ [[A]] |-> zero ]newstore
    s' = C[[Z:=1; if A=0 then diverge; Z:=3]]s₃
    in access [[Z]] s'
= let s₃ = [ [[A]] |-> zero ]newstore
    s₄ = [ [[Z]] |-> one ]s₃
    s' = C[[if A=0 then diverge; Z:=3]]s₄
    in access [[Z]] s'
= let s₃ = [ [[A]] |-> zero ]newstore
    s₄ = [ [[Z]] |-> one ]s₃
    s₅ = C[[if A=0 then diverge]]s₄
    s' = C[[Z:=3]]s₅
    in access [[Z]] s'

C[[if A=0 then diverge]]s₄
= B[[A=0]]s₄ -> C[[diverge]]s₄ [] s₄
= true -> C[[diverge]]s₄ [] s₄
= C[[diverge]]s₄
= (lambdas._|_)s₄
= _|_