Hi again.
Thank you very much for your help.
I read the solution that you posted and its a very interesting approach to the problem.
However, as part of my project, I'm trying to design this algorithm using an iteration through the possible values (from 1 to a, such that a<b).
This is my code so far, and I'm needing help to solve this problem using this approach: start the return variable with the value of a, and decreasing that value until I find a number that divides both a and b:
method mcd (a:nat, b:nat) returns (x:nat)
requires a>0
requires b>0
requires a<b
ensures x == Gcd(a, b)
{
var y:=1;
var A,B := a,b;
x:=1;
OneDividesAnything(a);
OneDividesAnything(b);
while y!=a
invariant Divides(x,A)
invariant Divides(x,B)
invariant x<=y
invariant forall k::(k>0 && k<=y && Divides(k,A) && Divides(k,B) ==> x>=k )
invariant y<=A
decreases A-y
{
var Y:=y;
if(DividesBoth(Y,A,B))
{ x:=y;}
}
y:= y+1;
}
function Gcd(a: int, b: int): int
requires a > 0 && b > 0
{
Exists(a, b);
var d :| DividesBoth(d, a, b) && forall m :: DividesBoth(m, a, b) ==> m <= d;
d
}
predicate DividesBoth(d: int, a: int, b: int)
requires a > 0 && b > 0
{
d > 0 && Divides(d, a) && Divides(d, b)
}
predicate {:opaque} Divides(d: int, a: int)
requires d > 0 && a > 0
{
exists n :: n > 0 && MulTriple(n, d, a)
}
predicate MulTriple(n: int, d: int, a: int)
requires n > 0 && d > 0
{
n * d == a
}
lemma Exists(a: int, b: int)
requires a > 0 && b > 0
ensures exists d :: DividesBoth(d, a, b) && forall m :: DividesBoth(m, a, b) ==> m <= d;
{
var d := ShowExists(a, b);
}
lemma ShowExists(a: int, b: int) returns (d: int)
requires a > 0 && b > 0
ensures DividesBoth(d, a, b) && forall m :: DividesBoth(m, a, b) ==> m <= d;
{
forall
ensures exists d :: DividesBoth(d, a, b)
{
OneDividesAnything(a);
OneDividesAnything(b);
assert Divides(1, a);
assert Divides(1, b);
assert DividesBoth(1, a, b);
}
d :| DividesBoth(d, a, b);
DividesUpperBound(d, a);
DividesUpperBound(d, b);
while true
invariant DividesBoth(d, a, b)
invariant d <= a && d <= b
decreases a + b - 2*d
{
if exists k :: DividesBoth(k, a, b) && k > d {
var k :| DividesBoth(k, a, b) && k > d;
d := k;
assert Divides(d, a);
DividesUpperBound(d, a);
assert d <= a;
DividesUpperBound(d, b);
assert d <= b;
} else {
return;
}
}
}
lemma OneDividesAnything(a: int)
requires a > 0
ensures Divides(1, a)
{
reveal_Divides(); // here, we use the definition of Divides
assert MulTriple(a, 1, a);
}
lemma DividesUpperBound(d: int, a: int)
requires d > 0 && a > 0
ensures Divides(d, a) ==> d <= a
{
reveal_Divides(); // here, we use the body of function Divides
}
I'm still getting errors and don't know why.
I would be very grateful if anybody could help me to solve this problem with this specific approach.
Thank you very much.
Alejandro Milieris