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
The effects of the concurrent assignment "Q,R:=Q+1,R-Y" are recorded in appropriate columns of the table (here, Q and R).