关于Dafny中IsPerfectSquare谓词的验证与表达问题

问题背景代码 #

IsPerfectSquare谓词实现 #

predicate IsPerfectSquare(n: int)
    requires n >= 0
{
    IsPerfectSquareFunctional(n, 0)
}

predicate IsPerfectSquareFunctional(n: int, sqrt_candidate: int) 
    requires n >= 0
    requires sqrt_candidate >= 0
    decreases n - sqrt_candidate
{
    // Unfortunately, this is not valid Dafny
    //exists k: int :: 0 <= k && k * k == n
    if sqrt_candidate * sqrt_candidate >= n then sqrt_candidate*sqrt_candidate == n
    else IsPerfectSquareFunctional(n, sqrt_candidate+1)
}

Main方法代码 #

method Main()
{
    for i:= 0 to 10
    {
        assert IsPerfectSquare(i*i);
    }
}

技术问题 #

1. 为何上述Main方法中的断言无法通过验证？
2. 是否可使用存在量词表达该谓词的后置条件？这是描述完全平方数的自然方式。

问题解答 #

1. 断言无法验证的原因 #

Dafny验证器无法自动推导递归谓词IsPerfectSquareFunctional的正确性与终止逻辑。这个递归谓词通过递增候选平方根直到其平方大于等于n来判断完全平方数，但验证器没办法自动证明：当输入为i*i时，递归会在候选值等于i时终止，且此时sqrt_candidate*sqrt_candidate == n成立。

你需要给递归谓词添加归纳引理或断言注解，辅助验证器理解递归的正确性。比如要证明：对于任意非负整数i，当候选值从0递增到i时，IsPerfectSquareFunctional(i*i, i)会返回true，且递归过程中每一步的前置条件都满足，递减量n - sqrt_candidate确实在持续减小。

2. 能否用存在量词表达谓词 #

完全可以，Dafny支持在谓词中直接使用存在量词，这也是描述完全平方数最自然的方式。之前注释里的写法是有效的，调整后直接定义即可：

predicate IsPerfectSquare(n: int)
    requires n >= 0
{
    exists k: int :: 0 <= k && k * k == n
}

这种写法下，验证器处理IsPerfectSquare(i*i)时，能直接找到k=i来满足断言，不需要额外的归纳证明，验证过程会更顺畅。

内容的提问来源于stack exchange，提问作者cvl