/* hardware integer division program, by Manna */

void division(int N, int D)
pre( N >= 0 && D > 0 );
    { 
    int r,ds,p,q;

    r=N;
    ds=D;
    p=1;
    q=0;

    inv( N >= 0 && D > 0 && q == 0 && r == N && ds == D*p && exists( int k; k>=0 && ds==D*2^k) && exists( int l; l>=0 && p==2^l ) );
    while ( r>= ds )
        {
        ds=2*ds;
        p=2*p;
        }

     inv( D > 0 && N == q*D+r && ds > r && r >= 0 && ds == D*p && exists( int k; k>=0 && ds==D*2^k) && exists( int l; l>=0 && p==2^l ) );
     while ( p!=1 )
         {
         ds=ds/2;
         p=p/2;

         if ( r>=ds ) 
             {
             r=r-ds;
             q=q+p;
             }
         }
    }
post( N == q*D+r && r >= 0 && r < D );