Gcd method with merge point specifications

Gcd.mps.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;

    //@ merge_point
    //@ merge_proc "MergeByIfThenElse"; // optional

    if (b < 0) b = -b;

    //@ merge_point
    //@ merge_proc "MergeByPredicateAbstraction"
    //@ merge_params {
    //@   conjunctive:
    //@   (int x) -> {x >= 0, (x == \old(b) || x == -\old(b))}
    //@ };

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

    return gcdHelp(big, small);
}