Trace Table: Symbolic Execution

compute symbolically
( R >= Y --> Q,R := Q+1,R-Y ) o ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )

We do this with a table for recording the effects of symbolically executing each statement of the function we are computing.

The table has one column or each variable involved in the computation. It also has one column for noting the current symbolic form of conditions when they are encountered.


  condition            Q               R             Y
  _____________________________________________________________
  R >= Y               Q+1             R-Y
  R-Y >= Y and Y > 0   (Q+1)+(R-Y)/Y   (R-Y) mod Y
  _____________________________________________________________
    ( R >= 2Y and Y > 0 --> Q, R := Q+R/Y, R mod Y

Of course, we can simplify these expressions some to get the final form.

Here, R-Y >= Y ==> R >= 2Y.
Also, (R-Y)/Y = R/Y - Y/Y = R/Y - 1.
Finally, (R-Y) mod Y = R mod Y.