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

Simplification II

let s3 = [ [[A]] |-> zero ]newstore
    s4 = [ [[Z]] |-> one ]s3
    s5 = C[[if A=0 then diverge]]s4
    s' = C[[Z:=3]]s5
    in access [[Z]] s'
= let s3 = [ [[A]] |-> zero ]newstore
    s4 = [ [[Z]] |-> one ]s3
    s5 = _|_
    s' = C[[Z:=3]]s5
    in access [[Z]] s'
= let s' = C[[Z:=3]]_|_
    in access [[Z]] s'
= let s' = (lambdas.update [[Z]] (E[[3]]s))_|_
    inaccess [[Z]] s'
= let s' = _|_
    inaccess [[Z]] s'
= access [[Z]] _|_
= _|_


Author: Wolfgang Schreiner
Last Modification: October 14, 1997

previous up next