Доказательство алгоритма GCD с Дафни - PullRequest
Новая
       27

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

1 голос
/ 25 июня 2019

Я пытаюсь доказать алгоритм 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 :: (0 < q3 <= result) && (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;
}

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

1 Ответ

0 голосов
/ 26 июня 2019

Мне удалось доказать более слабую 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;
}

Любые советы?

...