在 Dafny 中使用循环不变量内的方法答案

【问题标题】：Using methods inside loop invariants in Dafny在 Dafny 中使用循环不变量内的方法
【发布时间】：2019-06-25 04:24:20
【问题描述】：

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

【问题讨论】：

标签： dafny loop-invariant

【解决方案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 指南：函数的一个警告是，它们不仅可以出现在注释中，而且只能出现在注释中。函数永远不是最终编译程序的一部分，它们只是帮助我们验证代码的工具。

【讨论】：