Использование методов внутри циклических инвариантов в Dafny - PullRequest
Новая
       45

Использование методов внутри циклических инвариантов в Dafny

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

Я пытаюсь доказать простой алгоритм gcd в Dafny, поэтому я написал следующее, но, похоже, я не могу использовать метод divides внутри инвариантов цикла: 

method divides(d: int, x: int) returns (result: bool)
    requires d > 0
    requires x > 0
    ensures (result == true ) ==> (exists q : int :: (d * q == x))
    ensures (result == false) ==> (forall q : int :: (d * q != x))
{
    // code omitted
}

method gcd(a: int, b: int) returns (result: int)
    requires a > 0
    requires b > 0
    ensures (forall d : int :: ((exists q1 : int :: q1 * d == a) && (exists q2 :: (q2 * d == b))) ==>
                 (exists q3 : int :: (q3 * d == result)))
{
    var x := a;
    var y := b;
    var fuel := a+b;
    while ((x != y) && (fuel > 0))
        decreases fuel
        invariant x > 0
        invariant y > 0
        invariant (forall d : int :: (divides(d,x) && divides(d,y)) ==> (divides(d,a) && divides(d,b)))
    {
        // code omitted
    }
    return x;
}

Есть ли способ использовать divides метод / функцию / макрос внутри инвариантов?

...