/*@ predicate divisor(integer a, integer b) = 0 < a && 0 <= b && b%a == 0; predicate common_divisor(integer d, integer a, integer b) = divisor(d, a) && divisor(d, b); predicate gcd(integer d, integer a, integer b) = common_divisor(d, a, b) && (\forall integer z; common_divisor(z, a, b) ==> divisor(z, d)); lemma divisor1: \forall integer x; 0 <= x ==> divisor(1, x); lemma bar1: \forall integer a, b, x; common_divisor(x, a, b) ==> divisor(x, a + b); lemma bar: \forall integer a, b, x; 0 < b ==> common_divisor(x, a + b, b) ==> divisor(x, a); lemma X: (\forall integer a, b, x; 0 < b ==> common_divisor(x, a + b, b) ==> divisor(x, a)) ==> (\forall integer a, b, x; 0 < b < a ==> common_divisor(x, a, b) ==> divisor(x, a - b)); lemma foo: \forall integer a, b, x; 0 < b < a ==> common_divisor(x, a, b) ==> divisor(x, a - b); lemma foo1: \forall integer a, b, x; 0 < b < a ==> common_divisor(x, a - b, b) ==> divisor(x, a); */ /*@ requires 0 < x; requires 0 < y; assigns \nothing; ensures gcd(\result, x, y); */ int gcd(int x, int y) { int a = x; int b = y; /*@ loop invariant I: \forall integer t; common_divisor(t, x, y) <==> common_divisor(t, a, b); loop invariant pos: 0 < a; loop invariant pos: 0 < b; loop assigns a, b; loop variant a+b; */ while (a != b) { if (a > b) { //@ ghost L1: a -= b; } else { // ghost L2: b -= a; } } //@ assert gcd(a, x, y); return a; }