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 >= Y and R-Y >= Y and Y > 0 -->
Q, R := Q+1+(R-Y)/Y, (R-Y) mod Y )
We now write down the final function as a conditional assignment.
The conjunction of all entries in the "condition" column gives the domain restriction. The final entry in each column gives the new value for each variable.