基于Dafny的二维矩阵加法正确性证明及循环不变量问题

问题背景 #

想用VSCode的Dafny扩展证明二维矩阵加法的正确性，核心是找到能被SMT证明的循环不变量。实现了两层循环（外层遍历行，内层遍历列），但外层循环的不变量无法通过验证：

• 不添加断言时，Dafny提示this invariant could not be proved to be maintained by the loop
• 添加对应不变量的断言后，又提示assertion might not hold

原实现代码：

method Order2Addition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
    requires m1 != m3 && m2 != m3
    requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
    ensures CorrectMatrixAddition(m1, m2, m3)
    modifies m3
    {
        var rows: int := m1.Length0;
        assert(rows == m2.Length0 && rows == m3.Length0);
        var cols: int := m1.Length1;
        assert(cols == m2.Length1 && cols == m3.Length1);
        var i: int := 0;
        while (i < rows)
            invariant 0 <= i <= rows
            // All rows up to row i-1 are correct
            invariant forall i':int, j':int :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']
            decreases rows - i
            modifies m3
        {
            var j: int := 0;
            while (j < cols)
                invariant 0 <= j <= cols
                // All column values on row i, up to column j-1 are correct
                invariant forall j': int :: 0 <= j' < j ==> m3[i, j'] == m1[i, j'] + m2[i, j'] 
                decreases cols - j
                modifies m3
            {
                m3[i, j] := m1[i, j] + m2[i, j];
                j := j + 1;
            }
            i := i + 1;
            assert(forall i':int, j':int :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']);
        }
    }

predicate CorrectMatrixAddition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
    requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
    requires m1 != m3 && m2 != m3
    reads m1, m2, m3
{
    forall i: int, j: int {:trigger m3[i,j]} ::  0 <= i < m1.Length0 && 0 <= j < m1.Length1 ==> m3[i, j] == m1[i, j] + m2[i, j]
}

问题分析与修复 #

问题出在外层循环不变量的维护证明上：内层循环结束后，Dafny需要明确知道当前行i的所有列都已正确赋值，但原代码没有显式断言关联内层循环结果与外层循环不变量。

修复步骤 #

1. 在内层循环结束后添加断言，确认当前行完全正确
   内层循环结束时j == cols，此时需要断言当前行i的所有列都满足m3[i,j'] == m1[i,j'] + m2[i,j']，这是连接内外层循环不变量的关键。
2. 调整外层断言的位置
   把原断言移到i := i + 1之前，确保先确认当前行正确，再更新行索引i。

修复后的代码 #

method Order2Addition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
    requires m1 != m3 && m2 != m3
    requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
    ensures CorrectMatrixAddition(m1, m2, m3)
    modifies m3
    {
        var rows: int := m1.Length0;
        assert(rows == m2.Length0 && rows == m3.Length0);
        var cols: int := m1.Length1;
        assert(cols == m2.Length1 && cols == m3.Length1);
        var i: int := 0;
        while (i < rows)
            invariant 0 <= i <= rows
            invariant forall i':int, j':int :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']
            decreases rows - i
            modifies m3
        {
            var j: int := 0;
            while (j < cols)
                invariant 0 <= j <= cols
                invariant forall j': int :: 0 <= j' < j ==> m3[i, j'] == m1[i, j'] + m2[i, j'] 
                decreases cols - j
                modifies m3
            {
                m3[i, j] := m1[i, j] + m2[i, j];
                j := j + 1;
            }
            // 断言当前行i的所有列都已正确赋值
            assert forall j': int :: 0 <= j' < cols ==> m3[i, j'] == m1[i, j'] + m2[i, j'];
            // 先确认当前行正确，再更新行索引
            i := i + 1;
        }
    }

predicate CorrectMatrixAddition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
    requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
    requires m1 != m3 && m2 != m3
    reads m1, m2, m3
{
    forall i: int, j: int {:trigger m3[i,j]} ::  0 <= i < m1.Length0 && 0 <= j < m1.Length1 ==> m3[i, j] == m1[i, j] + m2[i, j]
}

原理说明 #

• 内层循环的不变量仅能保证到j-1列的正确性，循环结束时j=cols，显式断言整行正确后，Dafny才能将这个结果与外层循环不变量结合：外层循环要求所有i'<i的行正确，加上当前行i正确，就能推导出i自增后，所有i'<新i的行都正确，从而证明外层循环不变量的维护性。
• 调整断言位置后，i自增前的断言直接对应外层循环不变量需要的“新增行正确”条件，SMT求解器可以顺利完成推导。

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