public class Euclid {    
    /*@
      @ public normal_behavior  ....;
      @*/
    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 gcdHelper(big, small);
    }

    /*@
      @ public normal_behavior ...;
      @ assignable \nothing;
      @*/
    private static int gcdHelper(int _big, int _small) {
	int big = _big;
	int small = _small;
	/*@
	  @ loop_invariant ...;
	  @ decreases ...;
	  @ assignable ...;
	  @*/
	while (small != 0) {
	    final int t = big % small;
	    big = small;
	    small = t;
	}
	return big;
    }    
}