Dafny 循环不变式

Question

我正在 Dafny 中编写基于循环的平方根估计方法的代码，这就是我所拥有的：

method sqrt(val :int) returns (root:int)
requires val >= 0
ensures root * root >= val && (root - 1) * (root - 1) < val
{
        root := 0;
        var est := val;
        while (est > 0)
        invariant root * root >= val - est
        invariant (root-1) * (root-1) < val
        decreases est
        {
                root := root + 1;
                est := est - (2 * root - 1);
        }
}

由于循环不变性，Dafny 无法验证该程序。我有点明白为什么，我假设它是因为根可以是 0，因此 (0-1) * (0-1) < n could be false if n was 0, but I can't see a solution as I am new to this Dafny stuff. With the code described above I am getting an error when verifying which is:

src\dafnypractice.dfy(9,34)：错误：无法在输入时证明此循环不变式 相关消息：循环不变性违规 | 9 | 不变 (root-1) * (root-1) < val | ^

src\dafnypractice.dfy(9,34)：错误：无法证明该不变量是由循环维持的 相关消息：循环不变性违规 | 9 | 不变 (root-1) * (root-1) < val | ^

如有任何帮助，我们将不胜感激。

Answer 1

是的，您发现了一个不真实的案例。如果

val > 1

，您可以指定它，但是您需要开发这些案例。但是，您可以通过使其小于或等于 val 进行一些小的更改来使其工作。

    function toOdd(n: nat): nat
        requires n > 0
    {
        2*n-1
    }
    
    function SumOfNOddNumbers(n: nat): nat {
        if n == 0 then 0 else toOdd(n)+SumOfNOddNumbers(n-1)
    }

    lemma SumOddIsSquared(n: nat)
        ensures SumOfNOddNumbers(n) == n*n
    {}

    method sqrt(val :nat) returns (root:nat)
        ensures val == 0 ==> root == 0
        ensures val != 0 ==> (root - 1) * (root - 1) <= val
        ensures val != 0 ==> root * root >= val
    {
            root := 0;
            var est: int := val;
            while (est > 0)
                invariant val == 0 ==> root == 0
                // invariant est == val ==> root == 0
                invariant est == val-SumOfNOddNumbers(root)
                invariant root * root >= val - est
                invariant val != 0 ==> (root-1) * (root-1) <= val
                decreases est
            {
                    root := root + 1;
                    ghost var oldEst := est;
                    est := est - (2 * root - 1);
                    assert val != 0 ==> (root-1) * (root-1) <= val by {
                        // assert oldEst == val - SumOfNOddNumbers(root-1);
                        assert oldEst > 0;
                        SumOddIsSquared(root-1);
                    }
            }
    }
}