Go backward to Program Denotation Go up to Top Go forward to 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