将二维矩阵索引转一维数组索引的Dafny验证超时问题

我正在编写一个将二维矩阵索引转换为一维数组索引的Dafny方法，当前代码如下：

method calc_index(i: int, j: int, rows: int, cols: int) returns (index: int)
  requires 0 <= i < rows && 0 <= j < cols
  requires rows > 0 && cols > 0
  ensures 0 <= index < rows*cols
{
  assert 0 <= i < rows && 0 <= j < cols;
  index := (i * cols) + j;

}

现在遇到的问题是Dafny的验证在20秒后超时。我手动验证过转换逻辑是正确的，疑惑是否要验证的内容存在特殊复杂度？

解决建议 #

• 移除冗余断言：代码中的assert语句完全重复了前置条件，Dafny已经通过requires约束知晓这些条件成立，额外的断言会增加验证器的不必要计算，删除后可直接减轻验证负担。
• 添加分步推导断言：手动拆分计算步骤并补充中间范围断言，帮助Dafny简化推理路径，示例代码如下：

method calc_index(i: int, j: int, rows: int, cols: int) returns (index: int)
  requires 0 <= i < rows && 0 <= j < cols
  requires rows > 0 && cols > 0
  ensures 0 <= index < rows*cols
{
  let temp := i * cols;
  assert 0 <= temp < rows * cols;
  index := temp + j;
}

• 升级Dafny版本：旧版本的验证器在整数范围推理上效率偏低，升级至最新版通常能显著提升验证速度。

该转换逻辑本身复杂度不高，超时主要是验证器需要更明确的推理引导，或是冗余断言导致的额外计算开销。

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