0

我试图证明gcdDafny 中的简单算法，所以我写了以下内容，但似乎我不能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在不变量中使用方法/函数/宏？

4

1 回答 1

1

与方法不同，函数可以出现在表达式中。您可以创建一个函数：

function div(d: int, x: int): bool
{
    if (d != 0 && x % d == 0) then true else false
}

然后在你的方法divides中，你可以有

ensures result == div(d,x)

在您的方法中gcd，您可以在不变量中使用该函数div。

请注意，来自 Dafny 指南：功能的一个警告是，它们不仅可以出现在注释中，而且只能出现在注释中。函数永远不是最终编译程序的一部分，它们只是帮助我们验证代码的工具。

于 2020-03-18T19:09:35.040 回答