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);
        }
}

错误原因 #

• 循环入口验证失败：当val=0时，初始root=0，此时(root-1)*(root-1) = 1，1 < 0不成立，违反第二个循环不变量。
• 后置条件逻辑缺陷：当val=0时，返回root=0，但(0-1)*(0-1) < 0即1 < 0为假，不满足ensures定义的约束。
• 循环不变量精度不足：第一个不变量root * root >= val - est过于宽松，实际算法中root²严格等于val - est（奇数累加和为平方数：1+3+5+...+(2k-1)=k²），宽松的不变量会导致Dafny无法推导循环维护性。

修复方案 #

方案1：拆分特殊场景+精确不变量

单独处理val=0的情况，同时将第一个不变量改为精确等式，简化验证逻辑：

method sqrt(val :int) returns (root:int)
requires val >= 0
ensures root * root >= val && (root == 0 || (root - 1) * (root - 1) < val)
{
    if val == 0 {
        return 0;
    }
    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);
    }
}

方案2：调整不变量兼容边界场景

不拆分分支，通过条件判断让不变量和后置条件兼容val=0的场景：

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

说明 #

• 两种方案都修正了后置条件，确保val=0时逻辑自洽；
• 精确的循环不变量root * root == val - est能让Dafny清晰追踪变量间的数学关系，顺利完成循环维护性证明；
• 方案1逻辑更直白，方案2无需额外分支，可根据编码习惯选择。

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