-
Notifications
You must be signed in to change notification settings - Fork 0
/
gcd_partial.imp
37 lines (36 loc) · 1.23 KB
/
gcd_partial.imp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
gcd(m, n) {
(m % n = 0) ? n : gcd(n, m % n)
}
{x = X and y = Y and X > 0 and Y > 0}
|=
{x = X and y = Y and X > 0 and Y > 0 and x = X}
b := x
{x = X and y = Y and X > 0 and Y > 0 and b = X}
|=
{x = X and y = Y and X > 0 and Y > 0 and b = X and y = Y}
c := y
{x = X and y = Y and X > 0 and Y > 0 and b = X and c = Y}
|=
{gcd(x,y) = gcd(b,c) and b > 0 and c > 0 and x = X and y = Y}
while b # c do
{ b # c and (gcd(x,y) = gcd(b,c) and b > 0 and c > 0 and x = X and y = Y) }
if b < c then
{ b < c and (b # c and (gcd(x,y) = gcd(b,c) and b > 0 and c > 0 and x = X and y = Y)) }
|=
{gcd(x,y) = gcd(b,c - b) and b > 0 and c - b > 0 and x = X and y = Y}
c := c - b
{ gcd(x, y) = gcd(b, c) and b > 0 and c > 0 and x = X and y = Y}
else
{ not b < c and (b # c and (gcd(x,y) = gcd(b,c) and b > 0 and c > 0 and x = X and y = Y)) }
|=
{gcd(x,y) = gcd(b - c,c) and b - c > 0 and c > 0 and x = X and y = Y}
b := b - c
{gcd(x,y) = gcd(b,c) and b > 0 and c > 0 and x = X and y = Y}
end
{gcd(x,y) = gcd(b,c) and b > 0 and c > 0 and x = X and y = Y}
end
{not b # c and (gcd(x,y) = gcd(b,c) and b > 0 and c > 0 and x = X and y = Y)}
|=
{b = gcd(X, Y)}
z := b
{z = gcd(X, Y)}