/* Division algorithm from "Z. Manna, Mathematical Theory of Computation, McGraw-Hill, 1974" */

void division (int x1, int x2)
pre(  x1 >= 0   &&   x2 > 0  );
{
  int y1,y2,y3;

  y1 = 0;
  y2 = 0;
  y3 = x1;

  inv( y1* x2 + y2 + y3 == x1 );
  while(y3 != 0) {

    if (y2 + 1 == x2) {

      y1 = y1 + 1;
      y2 = 0;
      y3 = y3 - 1;
    }

    else {
      y2 = y2 + 1;
      y3 = y3 - 1;
    }
  }
}
post(  y2 == x1 % x2  &&  y1 == x1 / x2  );