Identity loop - 这个循环不变量可能不会被循环维护

Question

请检查下面我的代码。这个想法只是为每个数组位置添加一个常量（例如+1）。但是 dafny returns BP5005: This loop invariant might not be maintained by the loop. 对于 forall 条件。这对我来说没有多大意义，因为循环体完全按照我们在不变量中定义的方式执行。

Main 方法中的断言有效至关重要。

method doNothing(arr: array<int>)
modifies arr;
ensures arr.Length == old(arr.Length);
ensures forall i :: 0 <= i < arr.Length ==> arr[i] == (old(arr[i]) + 1);
{
  var idx: int := 0;

  while(idx < arr.Length)
  decreases arr.Length - idx;
  invariant 0 <= idx <= arr.Length;
  // # ERROR: BP5005: This loop invariant might not be maintained by the loop.Dafny VSCode
  invariant forall i :: 0 <= i < idx ==> arr[i] == (old(arr[i]) + 1);
  {
    arr[idx] := arr[idx] + 1;
    idx := idx + 1;
  }
}

method Main()
{
  var arr := new int[3];
  arr[0] := 1;
  arr[1] := 2;
  arr[2] := 3;

  doNothing(arr);

  assert(arr[0] == 2);
  assert(arr[1] == 3);
  assert(arr[2] == 4);
}

dafny 是否通过分配相同的值以某种方式更改了引用？？？

有人可以支持我吗？

谢谢指教。

Answer 1

您的循环不变量说明 arr[i] 和 old(arr[i]) 之间的关系，对于 0..idx 范围内的索引。但它没有说明 idx..a.Length 范围内索引的这种关系。因此，没有关于循环体赋值给arr[idx].

的arr[idx] + 1值的信息

Answer 2

好的，从我的快速坑中出来后，请看工作解决方案：感谢@Rustan

需要注意的关键是，我们不需要为 arr[idx] 显式创建 invarient，因为如果我们在body结束。

method doNothing(arr: array<int>)
modifies arr;
ensures arr.Length == old(arr.Length);
ensures forall i :: 0 <= i < arr.Length ==> arr[i] == old(arr[i]) + 1;
{

  var idx: int := 0;

  while(idx < arr.Length)
  decreases arr.Length - idx;
  invariant 0 <= idx <= arr.Length;
  // #INFO: no need, it's covered by the invariant below, evaluating at the body end.
  // invariant arr[idx] == old(arr[idx]) + 1;
  invariant forall j : int :: 0 <= j < idx ==> arr[j] == old(arr[j]) + 1;
  invariant forall j : int :: idx <= j < arr.Length ==> arr[j] == old(arr[j]);
  {
    // Evaluate Inv before loop body
    arr[idx] := arr[idx] + 1;
    idx := idx + 1;
    // Evaluate Inv after loop body => uses already updated idx value
  }
}
// neglect Main method

Identity loop - 这个循环不变量可能不会被循环维护

Identity loop - This loop invariant might not be maintained by the loop

arrays

while-loop

dafny