Created
February 24, 2020 14:38
-
-
Save pzp1997/535185f61983a4dc323f7a8c2d222ad3 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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; | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment