Dafny中矩阵乘法rowmul方法无法证明数组元素修改有效性问题

我正在验证矩阵乘法的过程，以下是我的Dafny代码：

predicate abvalid(a:array<array<int>>, b:array<array<int>>)
reads a, b
{
    a.Length > 0
    && b.Length > 0 
    && (forall i, j ::(0 <= i < a.Length && 0 <= j < a.Length) ==> (a[i].Length == a[j].Length == b.Length))
    && forall i, j :: (0 <= i < b.Length && 0 <= j < b.Length) ==> (b[i].Length == b[j].Length>0)
}


function rowcolmulAux(a:array<array<int>>, b:array<array<int>>, row:int, col:int, k :int) :int 
requires abvalid(a, b)
requires 0<=row < a.Length
requires 0<=col < b[0].Length
requires 0 <= k <= a[0].Length
decreases a[0].Length - k
reads a[..]
reads b[..]
reads a, b
ensures rowcolmulAux(a, b, row, col, k) == if k == a[0].Length then 0 else a[row][k] * b[k][col] + rowcolmulAux(a, b, row, col, k+1)
ensures (k == a[0].Length ==> rowcolmulAux(a, b, row, col, k) == 0) && (k < a[0].Length ==> rowcolmulAux(a, b, row, col, k) == a[row][k] * b[k][col] + rowcolmulAux(a, b, row, col, k+1))
{
    if k == a[0].Length then 0
    else a[row][k] * b[k][col] + rowcolmulAux(a, b, row, col, k+1)
}

function rowcolmul(a:array<array<int>>, b:array<array<int>>, row:int, col:int) :int 
reads a
reads b
reads a[..]
reads b[..]
requires abvalid(a, b)
requires 0<=row < a.Length
requires 0<=col < b[0].Length
ensures rowcolmul(a, b, row, col) == rowcolmulAux(a, b, row, col, 0)
ensures rowcolmul(a, b, row, col) == rowcolmul(a, b, row, col)
{
    rowcolmulAux(a, b, row, col, 0)
}
method rowmul(a:array<array<int>>, b:array<array<int>>, c1:array<int>, index:int, indexc: int)
requires abvalid(a, b)
requires 0 <= index < a.Length
requires c1.Length == b[0].Length
requires 0 <= indexc < c1.Length
modifies c1
ensures forall i :: 0 <= i < c1.Length && i != indexc ==> c1[i] == old(c1[i])
ensures c1[indexc] == rowcolmul(a, b, index, indexc)
{
    c1[indexc] := rowcolmul(a, b, index, indexc);
}

代码模块说明 #

• abvalid：校验矩阵a和b的合法性；
• rowcolmul与rowcolmulAux：计算输出矩阵单个元素的辅助函数；
• rowmul：将计算结果写入输出矩阵指定位置的方法。

遇到的问题 #

Dafny抛出验证错误：Could not prove: c1[indexc] == rowcolmul(a, b, index, indexc)

明明rowmul里只有一条赋值语句c1[indexc] := rowcolmul(a, b, index, indexc);，按道理这个等式必然成立，为什么验证器无法证明？

问题根源与修复方案 #

问题出在rowcolmul和rowcolmulAux的reads子句冗余，干扰了Dafny的依赖跟踪：

1. 冗余的reads声明：对于二维数组，reads a已经覆盖了数组本身及其所有元素的读取权限，额外添加reads a[..]属于重复声明，会让验证器对函数的读取范围产生混淆，无法明确rowcolmul的返回值仅依赖a和b的状态，且不受c1修改的影响。
2. 无意义的ensures语句：rowcolmul里的ensures rowcolmul(a, b, row, col) == rowcolmul(a, b, row, col)是恒真语句，对验证没有帮助，反而会分散验证器的注意力。

具体修复步骤：

1. 简化函数的reads子句，只保留必要的声明：

   function rowcolmulAux(a:array<array<int>>, b:array<array<int>>, row:int, col:int, k :int) :int 
   requires abvalid(a, b)
   requires 0<=row < a.Length
   requires 0<=col < b[0].Length
   requires 0 <= k <= a[0].Length
   decreases a[0].Length - k
   reads a, b  // 移除reads a[..]和reads b[..]
   ensures rowcolmulAux(a, b, row, col, k) == if k == a[0].Length then 0 else a[row][k] * b[k][col] + rowcolmulAux(a, b, row, col, k+1)
   {
       if k == a[0].Length then 0
       else a[row][k] * b[k][col] + rowcolmulAux(a, b, row, col, k+1)
   }
   
   function rowcolmul(a:array<array<int>>, b:array<array<int>>, row:int, col:int) :int 
   reads a, b  // 移除reads a[..]和reads b[..]
   requires abvalid(a, b)
   requires 0<=row < a.Length
   requires 0<=col < b[0].Length
   ensures rowcolmul(a, b, row, col) == rowcolmulAux(a, b, row, col, 0)
   {
       rowcolmulAux(a, b, row, col, 0)
   }
   

2. 删除rowcolmul中那行无意义的ensures语句。

修改后，Dafny验证器能清晰跟踪rowcolmul的依赖关系，确认赋值操作后c1[indexc]的值与rowcolmul的返回值完全一致，从而通过验证。

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