Method computing the Greatest Common Divisor (GCD) of two integers

Gcd.java

/*@ public normal_behavior
  @   ensures (a != 0 || b != 0) ==>
  @           (a % \result == 0 && b % \result == 0 &&
  @            (\forall int x; x > 0 && a % x == 0 && b % x == 0;
  @                            \result % x == 0));
  @*/
public static int gcd(int a, int b) {
    if (a < 0) a = -a;
    if (b < 0) b = -b;

    int big, small;
    if (a > b) {
        big = a;
        small = b;
    }
    else {
        big = b;
        small = a;
    }

    return gcdHelp(big, small);
}