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

Program Equivalence

C[[X:=0; Y:=X+1]] =^? C[[Y:=1;X:=0]]

• C: Store_{_|_} -> Store_{_|_}
• Show C[[C₁]]s = C[[C₂]]s for every s.
• C[[C₁]]_|_ = _|_ = C[[C₂]]_|_.

Assume proper store s.

C[[X:=0; Y:=X+1]]s
= C[[Y:=X+1]](C[[X:=0]]s)
= C[[Y:=X+1]]([ [[X]] |-> zero ]s)
= update [[Y]] (E[[X+1]]([ [[X]] |-> zero ]s))
    [ [[X]] |-> zero ]s
= update [[Y]] one [ [[X]] |-> zero ]s
= [ [[Y]] |-> one ][ [[X]] |-> zero ]s
= s₁