Dafny中两递归函数返回值正确但断言结果不一致求助

我编写了两个Dafny函数bullspec和bullspec2，用于计算两个序列中索引相同且值也相同的元素数量。两个函数仅递归方向不同：bullspec从序列尾部开始递归，bullspec2从头部开始递归。实际运行时两函数返回值均正确，但在Main方法中，assert bullspec(sys, usr) == 1断言不成立，assert bullspec2(sys, usr) == 1断言成立。尝试添加ensures语句但未解决问题，现寻求该断言差异的原因及解决办法。

相关代码 #

// bullspec函数
function bullspec(s:seq<nat>, u:seq<nat>): nat
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
{
  if |s| == 1 then (
    if s[0] in u && s[0] == u[0] 
    then 1 else 0
  ) else (
    if s[|s|-1] in u && s[|s|-1]==u[|s|-1] 
    then (1 + bullspec(s[..|s|-1], u))
    else bullspec(s[..|s|-1],u)
  )
}

// bullspec2函数
function bullspec2(s:seq<nat>, u:seq<nat>): nat
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
{
  if |s| == 1 then (
    if s[0] in u && s[0] == u[0] 
    then 1 else 0
  ) else (
    if s[0] in u && s[0] == u[0]
    then (1 + bullspec2(s[1..], u))
    else bullspec2(s[1..], u)
  )
}

// Main方法
method Main()
{
  var sys:seq<nat> := [4,2,9,3,1];
  var usr:seq<nat> := [1,2,3,4,5];

  assert bullspec(sys, usr) == 1; //Assertion might not hold
  assert bullspec2(sys, usr) == 1; //This is good
}

原因分析 #

1. 递归逻辑的验证难度差异：

   • bullspec2从头部递归，每次处理s的第一个元素后，递归调用s[1..]（去掉首元素的序列），验证器可以通过归纳法逐步推导：当前元素是否匹配，加上剩余序列的匹配数，逻辑链清晰，自动验证容易通过。
   • bullspec从尾部递归，每次处理s的最后一个元素后，递归调用s[..|s|-1]（去掉尾元素的序列），但u始终保持原序列不变。Dafny的验证器无法自动归纳出该递归调用与原函数功能的关联——它需要明确的断言来确认：递归调用的结果是s前缀与u对应前缀的匹配数。

2. 缺少明确的功能描述断言：
   尝试添加ensures但未解决问题，大概率是因为ensures没有精准描述函数的核心功能：即返回s和u中对应索引位置值相等的元素总数。没有这个断言，验证器无法建立递归步骤之间的逻辑联系。

解决办法 #

给bullspec添加精准的ensures断言，明确函数的功能，帮助验证器完成归纳证明：

function bullspec(s:seq<nat>, u:seq<nat>): nat
  requires 0 < |s| <= 10
  requires 0 < |u| <= 10
  requires |s| <= |u|
  // Remove duplicates
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j] && s[i] <= 10
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j] && u[i] <= 10
  // 明确函数功能：返回s和u中对应索引相等的元素数量
  ensures bullspec(s, u) == count i: nat | 0 <= i < |s| :: s[i] == u[i]
{
  if |s| == 1 then (
    if s[0] == u[0]
    then 1 else 0
  ) else (
    let lastIdx := |s| - 1;
    if s[lastIdx] == u[lastIdx] 
    then (1 + bullspec(s[..lastIdx], u))
    else bullspec(s[..lastIdx], u)
  )
}

补充说明：

• count i: nat | 0 <= i < |s| :: s[i] == u[i]是Dafny内置的计数表达式，直接描述了函数要实现的功能。
• 原代码中s[lastIdx] in u的判断是多余的（因为即使元素不在u中，s[lastIdx] == u[lastIdx]也会是false），可以删除以简化逻辑，不影响结果。
• 添加该ensures后，Dafny验证器可以通过归纳法证明递归步骤的正确性，进而通过Main中的断言。

内容的提问来源于stack exchange，提问作者Giang Hoa Tran