5 - División Entera Mejorada (p.138)

[ var x,y,q,r,d,dd: Int
$\{R: x\geq 0 \wedge y\geq 0\}$ 
q,r := 0,x
$\{Q: x=q\times y+r \wedge 0\leq r\}$ 
 do
	r$\geq$y $\rightarrow$ d,dd := 1,y 
		 do
			r$\geq 2\times$dd $\rightarrow$ d,dd := $2\times$d,$2\times$dd 
		 od
		q,r := q+d,r-dd
 od
$\{Q: x=q\times y+r \wedge 0\leq r \wedge r<y\}$ 
]