Suppose that the factorial function is defined as follows.
  Define
    factorial(n: Integer): Integer by

    factorial(n) = r |
      Let r = 1.
      Let k = 2.
      While k <= n do
        Relet r = r * k.
        Relet k = k + 1.
      %While
  %Define
Do a careful hand simulation of factorial(4).