V V or V'with V ranging over sets of variables.
From this information, we can construct (S,H,is) as follows:
Initial configuration (Fig 2.15) | ||||||||
x @ @ @ |
x is a list with at least two elements | |||||||
1: y := nil | ||||||||
x @ @ @ |
||||||||
Merge with the end of loop body (that is, output from 6) | ||||||||
x @ @ @ |
y x @ @ @ |
y x @ @ |
y x @ z @ @ |
x y @ z @ |
y @ z @ |
z y x @ @ z @ @ |
z y @ x @ z @ |
y z @ z @ @ |
2: not is-nil(x) (true-branch) | ||||||||
x @ @ @ |
y x @ @ @ |
y x @ @ |
y x @ z @ @ |
x y @ z @ |
z y x @ @ z @ @ |
z y @ x @ z @ |
||
3: z := y | ||||||||
x @ @ @ |
yz x @ @ @ |
zy x @ @ |
zy x @ @ @ @ |
zy @ x @ @ |
identical to previous | |||
4: y := x | ||||||||
xy @ @ @ |
z yx @ @ @ |
z yx @ @ |
z xy @ @ @ @ |
z @ yx @ @ |
||||
Realigning the above | ||||||||
xy @ @ @ |
z yx @ @ @ |
z yx @ @ |
z xy @ @ @ @ |
z @ yx @ @ |
||||
5.1: t := x.cdr | ||||||||
xy t @ t @ @ |
xy @ t @ |
z yx t @ t @ @ |
z yx @ t @ |
z yx @ @ |
z xy t @ @ t @ @ |
z xy @ @ t @ |
z @ xy @ @ |
|
5.2: x := t | ||||||||
y xt @ xt @ @ |
y xt @ xt @ |
z y xt @ xt @ @ |
z y @ xt @ |
z y @ @ |
z y xt @ @ xt @ @ |
z y @ @ xt @ |
z @ y @ @ |
|
5.3: t := nil | ||||||||
y x @ x @ @ |
y x @ x @ |
z y x @ x @ @ |
z y @ x @ |
z y @ @ |
z y x @ @ x @ @ |
z y @ @ x @ |
z @ y @ @ |
|
6: y.cdr := z | ||||||||
y x @ @ @ |
y x @ @ |
y x @ z @ @ |
x y @ z @ |
y @ z @ |
z y x @ @ z @ @ |
z y @ x @ z @ |
y z @ z @ @ |
|
End of loop (false-branch of 2): | ||||||||
y @ z @ |
y z @ z @ @ |
|||||||
7: z := nil | ||||||||
y @ @ @ |
y is a list with at least two elements |