Go backward to Simplification
Go up to Top
Go forward to Simplification
|
Go backward to Simplification Go up to Top Go forward to Simplification |
|
C[[if A=0 then
diverge; Z:=3]](C[[Z:=1]]s1)
= C[[if A=0 then diverge; Z:=3]]s2
= (lambdas.C[[Z:=3]](C[[if A=0
then diverge]]s)s2
= (lambdas.C[[Z:=3]]((lambdas.B[[A=0]]s ->
C[[diverge]]s [] s) s))s2
= C[[Z:=3]]((lambdas.B[[A=0]]s
->
C[[diverge]]s [] s)s2)
= C[[Z:=3]](B[[A=0]]s2 ->
C[[diverge]]s2 [] s2)
B[[A=0]]s2
= (lambda s.E[[A]]s equals E[[0]]s)s2
= E[[A]]s2 equals E[[0]]s2
= (access [[A]] s2) equals zero
access [[A]] s2
= s2 [[A]]
= ( [ [[Z]] |-> one ][ [[A]] |-> two ]
newstore ) [[A]]
= ([ [[A]] |-> two ] newstore) [[A]]
= two