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

As before, the effects of the concurrent assignment are entered in the columns for the variables assigned. Here, for example, the new value of Q is Q+R/Y. Symbolically, the current value of Q is Q+1, and the value of R is R-Y. Substituting these symbolic values into "Q+R/Y" gives "(Q+1)+(R-Y)/Y" as the new value for Q (we use parentheses for clarity).