如何在Dafny中用函数统计两序列同索引相等元素的数量

Dafny的函数属于纯函数范畴，无法使用while循环这类命令式语句，因此可以通过递归或内置高阶函数实现需求，以下是两种可行方案：

方法1：递归实现 #

递归是Dafny函数中处理序列遍历的常规方式，通过逐步缩小序列规模完成统计：

function test(s: seq<nat>, u: seq<nat>): nat
  requires |s| == |u|  // 约束两个序列长度必须相等
{
  if |s| == 0 then
    0  // 空序列无元素可比较，返回0
  else
    // 检查最后一个元素是否相等，累加前n-1个元素的统计结果
    (if s[|s|-1] == u[|u|-1] then 1 else 0) + test(s[0..|s|-1], u[0..|u|-1])
}

逻辑说明 #

• 终止条件：当序列长度为0时，直接返回0，无元素需要比较。
• 递归步骤：每次取出两个序列的末尾元素对比，相等则加1，再递归处理去掉末尾元素的子序列，最终累加得到相等元素的总数。

方法2：使用内置Count函数结合序列推导式 #

利用Dafny内置的Count函数统计符合条件的元素数量，先构造布尔序列记录同索引元素的相等状态，再统计其中true的数量：

function test(s: seq<nat>, u: seq<nat>): nat
  requires |s| == |u|
{
  // 生成布尔序列，每个元素对应原序列同索引元素是否相等，再统计true的数量
  Count(seq(i: nat | i < |s| :: s[i] == u[i]), b => b)
}

逻辑说明 #

• seq(i: nat | i < |s| :: s[i] == u[i])：通过序列推导式生成布尔序列，每个位置i的值为s[i]与u[i]是否相等的判断结果。
• Count(..., b => b)：统计该布尔序列中true的数量，即同索引相等元素的总数。

验证示例 #

针对你提供的测试代码，两种实现均能满足断言要求：

method Testing()
{
  var sys: seq<nat> := [4,2,9,3,1];
  var usr: seq<nat> := [1,2,3,4,5];
  assert test(sys, usr) == 1;  // 仅0-based索引1的元素值为2，两者相等
}

注：你注释中提到的“索引2”是1-based计数，对应Dafny的0-based索引1，两种实现的统计结果均为1，符合预期。

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