Proving gcd algorithm with Dafny

Question

I'm trying to prove the gcd algorithm with Dafny and it's apparently not that simple. What I have so far (not much indeed) is a functional specification, and Dafny manages to prove that compute_gcd behaves like it. However, when I remove the comments [1], [2] and [3] Dafny fails to prove that the functional specification has the desired properties:

function gcd(a: int, b: int) : (result : int)
    requires a > 0
    requires b > 0
    // [1] ensures (exists q1:int :: (q1 * result == a))
    // [2] ensures (exists q2:int :: (q2 * result == b))
    // [3] ensures forall d :int, q1:int, q2:int :: ((q1*d==a)&&(q2*d==b)) ==> (exists q3:int :: (q3*d == result))
{
    if (a >  b) then gcd(a-b,b) else
    if (b >  a) then gcd(a,b-a) else a
}

method compute_gcd(a: int, b: int) returns (result: int)
    requires a > 0
    requires b > 0
    ensures result == gcd(a,b)
{
    var x := a;
    var y := b;
    while (x != y)
        decreases x+y
        invariant x > 0
        invariant y > 0
        invariant gcd(x,y) == gcd(a,b)
    {
        if (x > y) { x := x - y; }
        if (y > x) { y := y - x; }
    }
    return x;
}

Am I going in the right direction? any help is very much appreciated, thanks!

Answer 1

You might take a look at the GCD algorithm in the Dafny test suite (in Test/VerifyThis2015/Problem2.dfy) and compare it with your approach:

Answer 2

I managed to prove a weaker gcd specification (permalink here), but I'm still having a hard time with property [3] above:

function gcd(a: int, b: int) : (result : int)
    requires a > 0
    requires b > 0
    // [1] ensures (exists q1:int :: (q1 * result == a))
    // [2] ensures (exists q2:int :: (q2 * result == b))
{
    if (a > b) then gcd(a-b,b) else
    if (b > a) then gcd(a,b-a) else a
}

lemma gcd_correct(a: int, b: int)
    requires a > 0
    requires b > 0

    ensures (exists q1:int :: (q1 * gcd(a,b) == a))
    ensures (exists q2:int :: (q2 * gcd(a,b) == b))
{
    if (a > b)
    {
        gcd_correct(a-b, b);
        var q1 :| q1 * gcd(a-b,b) == a-b;
        var q2 :| q2 * gcd(a-b,b) == b;
        assert (q1+q2) * gcd(a,b) == a;
    }
    else if (b > a)
    {
        gcd_correct(a,b-a);
        var q1 :| q1 * gcd(a,b-a) == a;
        var q2 :| q2 * gcd(a,b-a) == b-a;
        assert (q2+q1) * gcd(a,b) == b;
    }
    else
    {
        assert 1 * gcd(a,b) == a;
    }
}

method compute_gcd(a: int, b: int) returns (result: int)
    requires a > 0
    requires b > 0
    ensures result == gcd(a,b)
    ensures (exists q1:int :: (q1 * result == a))
    ensures (exists q2:int :: (q2 * result == b))
{
    var x := a;
    var y := b;
    while (x != y)
        decreases x+y
        invariant x > 0
        invariant y > 0
        invariant gcd(x,y) == gcd(a,b)
    {
        if (x > y) { x := x - y; }
        if (y > x) { y := y - x; }
    }
    gcd_correct(a,b);
    return x;
}

Any tips?