Program Equivalence
C[[Y:=1; X:=0]]s
= C[[X:=0]](C[[Y:=1]]s)
= C[[X:=0]]([ [[Y]] |-> one ]s)
= [ [[X]] |-> zero ][ [[Y]] |-> one ]s
= s2
- s1 =? s2.
- s1,s2: Id -> Nat
- Show s1(id) = s2(id) for every id.
- id = [[X]]: s1[[X]] = ([ [[Y]] |-> one
][ [[X]] |-> zero ]s)[[X]] = ([[X]] |-> zero
]s)[[X]] = zero = ([ [[X]] |-> zero ][ [[Y]]
|-> one ]s)[[X]] = s2[[X]].
- id = [[Y]]: s1[[Y]] = ([ [[Y]] |->
one
][ [[X]] |-> zero ]s)[[Y]] = one = ([ [[Y]]
|-> one ]s)[[Y]] = ([ [[X]] |-> zero
][ [[Y]] |-> one ]s)[[Y]] = s2[[Y]].
- id = [[I]]: s1[[I]] = ([ [[Y]] |-> one
][ [[X]] |-> zero ]s)[[I]] = ([ [[X]] |->
zero ]s)[[I]] = s[[I]] = ([ [[Y]] |-> one ]s)[[I]]
= ([ [[X]] |-> zero ][ [[Y]] |-> one
]s)[[I]] = s2[[I]].
Author: Wolfgang Schreiner
Last Modification: October 14, 1997