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
  _____________________________________________________________

In this case, the code is changing the values of variables Q and R. We put Y in the table to show that it remains unchanged.