Greatest common divisor

Jun 27, 2015 at 9:05 PM
Hi everybody.

I'm starting to learn Dafny and as a beggining I'm trying to solve a bunch of common problems with integers, and I'm getting many errors in simple stuff, that I don't know how to solve.
For example: Greatest common divisor (GCD).

I'm trying to write a method to get the GCD of two numbers a and b (a<=b).
I want the method to return x, such that x divides a and b, and ensures that there is no number greater than x that divides both a and b.
The highest possible value that x can be is a, in the case that a divides b.
So, I initialize x=a.
Then, while x doesn't divides both a and b, I decrease x in a while loop.
My invariant is that there is no number greater that x that divides both a and b.
I tried to do this simple algorithm as a function, as a method, or as a function method, and still doesn't work.

Here is my code:

predicate divides (x:nat, y:nat)
{x==y==0 || x==1 ||(x!=0 && x<=y && y%x == 0)}

function method Mcd (a:nat, b:nat) :nat
requires a<b
ensures divides(x,a)
ensures divides(x,b)
ensures forall z :: z>x ==> !( divides(z,a) && divides(z,b))
{
var x:nat :=a;
while !(divides(x,a) && divides(x,b))
invariant forall z :: z>x ==> !(divides(z,a) && divides(z,b))
decreases x
{
x:=x-1;
}
}

And I'm getting this error: stdin.dfy(11,3): error: invalid UnaryExpression
1 parse errors detected in stdin.dfy

I would appreciate a lot any answer that can help me, so I can move forward to more complex algorithms. Feel free to contact me: milierisalejandro@gmail.com Thank you very much,

Alejandro Milieris
Jun 28, 2015 at 8:41 AM

You may have some problems with the SMT solver and the '%' operator, there is a test case in the Dafny tests with a full solution to a similar problem which I have linked below. Instead of '%' it uses the fact that 'd' divides 'a' iff there exists an 'n' such that 'd*n=a'

*spoiler* here is the solution from the Dafny tests:

https://dafny.codeplex.com/SourceControl/latest#Test/VerifyThis2015/Problem2.dfy

Jun 28, 2015 at 10:34 PM
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