如何证明修改二维数组元素时其余元素保持不变？

你的问题出在Dafny无法自动推导出未被modifies声明的子数组完全未发生变化。断言A只针对被修改的那一行（arr[index1]），验证逻辑单一所以能通过；但断言B覆盖整个二维数组，当some_index1 != index1时，Dafny需要明确知道arr[some_index1]和修改前的old(arr[some_index1])是同一个数组对象，才能确定它的所有元素都和原来一致。

解决方法 #

在修改元素之后、断言B之前，添加一个中间断言，明确告诉验证器：除了index1对应的子数组，其他子数组都和修改前的引用完全相同：

method modify_array_element(arr: array<array<nat>>, index1: nat, index2: nat, val: nat)
  requires index1 < arr.Length
  requires index2 < arr[index1].Length
  modifies arr[index1]
  ensures forall some_index1: nat, some_index2: nat ::
        some_index1 < arr.Length && some_index2 < arr[some_index1].Length ==>
    arr[some_index1][some_index2] == if index1 == some_index1 && index2 == some_index2
        then val else old(arr[some_index1][some_index2])
{
    arr[index1][index2] := val;
    // assert statement A
    assert forall some_index2: nat :: some_index2 < arr[index1].Length ==>
        arr[index1][some_index2] == if index2 == some_index2
            then val else old(arr[index1][some_index2]);
    // 新增断言：未被修改的子数组与原数组引用一致
    assert forall i: nat :: i < arr.Length && i != index1 ==> arr[i] == old(arr[i]);
    // assert statement B
    assert forall some_index1: nat, some_index2: nat ::
        some_index1 < arr.Length && some_index2 < arr[some_index1].Length ==>
        arr[some_index1][some_index2] ==
            if index1 == some_index1 && index2 == some_index2
            then val else old(arr[some_index1][some_index2]);
}

原理说明 #

• Dafny的modifies子句仅声明哪些对象会被修改，但不会自动推断未被声明对象的状态。这里modifies arr[index1]只告诉验证器我们会修改第index1个子数组，但其他子数组的引用是否保持不变，需要显式断言。
• 当arr[i] == old(arr[i])时，Dafny会自动推导这个子数组的所有元素都和修改前一致，结合断言A的结论，就能覆盖断言B的所有情况，让验证通过。

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