Spring 2001 CS100M -- detailed trace of E5.2

here is the code from E5.2, with some additional line#s:

1      x = 6; y = 11; X = x; Y = y; z = 0;
       % inv: X*Y = x*y + z
1.1    while x ~=0 & y ~= 0
1.2        if x < y
2              t = x;
3              x = y;
4              y = t;
4.1        end
4.2        if rem(y,2) == 0
5              x = x+x;
6              y = y/2;
6.1        else
7              z = z+x;
8              y = y-1;
8.1        end
9      end

here is the tabular trace that was provided:

snapshot:  (a) (b)  (c) (d)  (e) (f)  (g) (h)  (i) (k)  (l) (m)
            |   |    |   |    |   |    |   |    |   |    |   |
       #  1 | 2 |  3 | 4 |  5 | 6 |  7 | 8 |  5 | 6 |  7 | 8 |
       X  6 |   |    |   |    |   |    |   |    |   |    |   |
       Y 11 |   |    |   |    |   |    |   |    |   |    |   |
       x  6 |   | 11 |   | 22 |   |    |   | 44 |   |    |   |
       y 11 |   |    | 6 |    | 3 |    | 2 |    | 1 |    | 0 |
       z  0 |   |    |   |    |   | 22 |   |    |   | 66 |   |
       t    | 6 |    |   |    |   |    |   |    |   |    |   |

here is a detailed explanation of how the code is executed:

line #1   is executed: we are now at snapshot (a)
line #1.1 is executed: loop guard is true, so execute loop body
line #1.2 is executed: condition x<y is true, so execute conditional's body
line #2   is executed: we are now at snapshot (b)
line #3   is executed: we are now at snapshot (c)
line #4   is executed: we are now at snapshot (d)
line #4.1 is reached:  we have reached end of conditional; 
                       we continue executing after the conditional
line #4.2 is executed: condition rem(6,2) == 0 is true, so execute $if$ clause
line #5   is executed: we are now at snapshot (e)
line #6   is executed: we are now at snapshot (f)
line #6.1 is reached:  we have reached the end of the $if$ clause, so
                       we must skip past the end of the conditional, to:
line #9   is reached:  we have reached the end of the loop body, so
                       we go back to the start of the loop
line #1.1 is executed: loop guard is true, so execute loop body
line #1.2 is executed: condition x<y is false, so skip past end of conditional
                       which takes us to:
line #4.2 is executed: condition rem(3,2) == 0 is false, so go to $else$ clause
line #6.1 is reached
line #7   is executed: we are now at snapshot (g)
line #8   is executed: we are now at snapshot (h)
line #8.1 is reached:  we have reached the end of conditional,
                       so continue execution after the conditional:
line #9   is reached:  we have reached the end of the loop body, so
                       we go back to the start of the loop
line #1.1 is executed: loop guard is true, so execute loop body
line #1.2 is executed: condition x<y is false, so skip past end of conditional
                       which takes us to:
line #4.2 is executed: condition rem(3,2) == 0 is true, so execute $if$ clause
line #5   is executed: we are now at snapshot (i)
line #6   is executed: we are now at snapshot (k)
line #6.1 is reached:  we have reached the end of the $if$ clause, so
                       we must skip past the end of the conditional, to:
line #9   is reached:  we have reached the end of the loop body, so
                       we go back to the start of the loop
line #1.1 is executed: loop guard is true, so execute loop body
line #1.2 is executed: condition x<y is false, so skip past end of conditional
                       which takes us to:
line #4.2 is executed: condition rem(1,2) == 0 is false, so go to $else$ clause
line #7   is executed: we are now at snapshot (l)
line #8   is executed: we are now at snapshot (m)
line #8.1 is reached:  we have reached the end of conditional,
                       so continue execution after the conditional:
line #9   is reached:  we have reached the end of the loop body, so
                       we go back to the start of the loop
line #1.1 is executed: loop guard is false, so do NOT execute loop body;
                       instead, skip past end of the loop, i.e. after line#9