Reaching Definitions

(x,?), (y,?), (z,?)

(x,?), (y,1), (z,?)

(x,?), (y,1), (z,2), (y,5), (z,4)

[y := x]1;

[z := 1]2;

while [yɭ]3

do ( [z := z*y]4;

[y := y-1]5

);

[y := 0]6

(x,?), (y,6), (z,2), (z,4)

Another safe solution - but not the best: