previous up next
Go backward to Program Denotation
Go up to Top
Go forward to Simplification
RISC-Linz logo

Simplification

P[[Z:=1; if A=0 then diverge; Z:=3.]](two)
= let s1 = (update [[A]] two newstore)
    s' = C[[Z:=1; if A=0 then diverge; Z:=3]]s1
    in access [[Z]] s'
= let s1 = ( [ [[A]] |-> two ] newstore)
    s' = C[[Z:=1; if A=0 then diverge; Z:=3]]s1
    in access [[Z]] s'

C[[Z:=1; if A=0 then diverge; Z:=3]]s1
= (lambdas.C[[if A=0 then diverge; Z:=3]]
    (C[[Z:=1]]s))s1
= C[[if A=0 then diverge; Z:=3]](C[[Z:=1]]s1)

C[[Z:=1]]s1
= (lambdas.update [[Z]] (E[[1]]s) s)s1
= update [[Z]] (E[[1]]s1) s1
= update [[Z]] (N[[1]]) s1
= update [[Z]] one s1
= [ [[Z]] |-> one ]s1
= s2


Author: Wolfgang Schreiner
Last Modification: October 14, 1997

previous up next