// @(#)$Id: Euclid.C,v 1.2 1999/04/12 17:06:23 leavens Exp $
#include <stdlib.h>

//@ uses gcd(int for Int);

int Euclid(int X, int Y) throw()
{
  //@ requires X^ \neq 0 \/ Y^ \neq 0;
  int x = abs(X);
  int y = abs(Y);
  //@ assert x' == abs(X^) /\ y' == abs(Y^);
  //@ assert redundantly x' \neq 0 \/ x' \neq 0;

  //@ maintaining gcd(x', y') == gcd(X^, Y^)
  //@ decreasing abs(y' - x')
  while (x != y) {
    if (x > y) {
      x = x - y;
    } else {
      //@ assert y' > x';
      y = y - x;
    }
  }
  //@ assert x' == y';

  //@ ensures x' == gcd(X^,Y^);
  return x;
}