Assume programs uses just D_1,D_2 for declarations.
- Copy rule:
- define I_1=V_1, ..., define I_n=V_n
in U
=> [V_1/I_1, ..., V_n/I_n]U.
- Bodies V_j are substituted for invocations I_j in U.
- Simultaneous substitutions V_j/I_j.
- Example:
- fun A=1, fun B=@loc_1=0
in
while B do loc_1:=A+2 od
=>
[1/A, @loc_1=0/B]
while B do
loc_1:=A+2 od
=
while @loc_1=0 do
loc_1:=1+2 od
Easy to handle.