public class GCD { /*@ @ requires a>=0 && b>=0; @ ensures \result >= 0; @ ensures (\exists int q; \result*q == a) && @ (\exists int q; \result*q == b) && @ (\forall int c; @ (\exists int q; c*q == b) && (\exists int q; c*q == a); @ (\exists int q; c*q == \result)); @*/ public static int gcd(int a, int b) { /*@ loop_invariant a >= 0 && b>=0 && @ (\forall int d; @ (\exists int q; \old(a) == q*d) && (\exists int q; \old(b) ==q*d) @ <==> @ (\exists int q; a == q*d) && (\exists int q; b ==q*d)); @ assignable a,b; @ decreases a+b; @*/ while (a != 0 && b != 0) { if (a > b) a = a - b; else b = b - a; } return (a > b) ? a : b; } }