Dafny多decreases子句生效规则疑问：Bug还是预期行为？

首先看你提到的原函数：

function K(x: nat, y: nat, z: nat): int
{
    if x < 10 || y < 5 
    then x + y
    else if z == 0
        then K(x-1, y, 5)
        else K(x, y-1, z-1)
}

这是Dafny的预期行为，并非Bug，核心原因在于Dafny对多个decreases子句的处理逻辑：

• 多个decreases子句会被组合成一个字典序的多元终止度量，递归调用只需满足该多元度量在字典序上严格小于当前值即可，而非要求每个子句单独满足终止条件。

具体分析 #

原函数的递归分支分为两种情况：

1. 当z==0时，调用K(x-1, y, 5)
2. 当z!=0时，调用K(x, y-1, z-1)

单独使用decreases 5*(x+y)+z验证失败的原因

在z==0的分支中：

• 当前度量值：5*(x+y)+0 = 5x+5y
• 递归后的度量值：5*((x-1)+y)+5 = 5x+5y-5+5 = 5x+5y
  两者完全相等，不满足严格递减的终止要求，因此验证失败。

添加decreases x+y后验证通过的原因

此时Dafny将两个子句组合为多元度量(5*(x+y)+z, x+y)，分别检查两个递归分支：

• z==0分支：递归后的多元度量为(5*(x+y), x+y-1)，与当前的(5*(x+y), x+y)相比，第一个元素相等，但第二个元素严格减小，符合字典序递减规则。
• z!=0分支：递归后的多元度量第一个元素为5*(x+(y-1))+(z-1) = 5*(x+y)+z-6，比当前值5*(x+y)+z更小，直接满足字典序递减。

整个多元度量覆盖了所有递归场景的终止要求，因此验证通过。

其他有效度量的原理

• decreases x+y：两个递归分支的x+y都会严格减1，自然满足终止条件。
• decreases 6*(x+y)+z：z==0分支的递归度量为6*((x-1)+y)+5 = 6*(x+y)-1，比当前值6*(x+y)小，满足严格递减。

内容的提问来源于stack exchange，提问作者A. Meijster