Доказательство алгоритма НОД с Дафни

Я пытаюсь доказать алгоритм gcd с Дафни, и это, видимо, не так просто. На данный момент у меня есть (на самом деле немного) функциональная спецификация, и Дафни удалось доказать, что compute_gcd ведет себя именно так. Однако, когда я удаляю комментарии, [1], [2] and [3] Дафни не может доказать, что функциональная спецификация имеет желаемые свойства:

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;
}

Я иду в правильном направлении? любая помощь очень ценится, спасибо!


greatest-common-divisor dafny
person OrenIshShalom    schedule 25.06.2019    source источник

Ответы (2)


arrow_upward
0
arrow_downward

Мне удалось доказать более слабую спецификацию gcd (постоянная ссылка здесь), но мне все еще тяжело со свойством [3] выше:

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;
}

Какие-нибудь советы?

person OrenIshShalom    schedule 26.06.2019

arrow_upward
0
arrow_downward

Вы можете взглянуть на алгоритм GCD в наборе тестов Dafny (в Test/VerifyThis2015/Problem2.dfy) и сравните его со своим подходом:

person Bryan Parno    schedule 29.07.2019