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
The condition R >= Y is recorded in the table, using the
"current" values of the variables.
Looking up the columns
for each variable, we see none have changed from their
initial values.