EuclidAlgo.jml

public class EuclidAglo {
    // cd(x, y, z) <==> (x % z == 0) && (y % z == 0)
    // gcd(x, y, z) <==> cd(x, y, z) && (\forall int k;; cd(x, y, k) ==> k <= z)
    
    //@ requires true;
    //@ ensures (x % \result == 0) && (y % \result == 0) && (\forall int k;; (x % k == 0) && (y % k == 0) ==> k <= \result);
    public static int run(int x, int y) {
      int n = x;
      int m = y;
      //@ maintaining (\forall int z;; ((x % z == 0) && (y % z == 0) && (\forall int k;; (x % k == 0) && (y % k == 0) ==> k <= z)) <==> ((n % z == 0) && (m % z == 0) && (\forall int k;; (n % k == 0) && (m % k == 0) ==> k <= z)));
      //@ decreases n;
      while (n != m) {
        if (n > m) {
          n -= m;
        } else {
          m -= n;
        }
      }
      return n;
    }
}