previous up next
Go backward to Program Equivalence
Go up to Top
Go forward to Programs Are Functions
RISC-Linz logo

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


Author: Wolfgang Schreiner
Last Modification: October 14, 1997

previous up next