{a>=0 & d>0}
{                                                                    }
r:=a;
q:=0;
{                                                                    }
while r>=d do
{inv.                                                                }
{                                                                    }
    begin
    {								     }
    dd:=d;
    qq:=1;
    {                                                                }
    while r>=dd do
    {inv.                                                            }
    {                                                                }
        begin
        {							     }
        r:=r-dd;
        dd:=dd+dd;
        {                                                            }
        q:=q+qq;
        qq:=qq+qq
        {                                                            }
        end
        {                                                            }
    end
{                                                                    }
{d*q+r=a & 0<=r<d }