为什么这个涉及数组的 Dafny 断言会失败？

Question

我正在研究经过验证的高斯消除实现，但在验证这种将数组 b 的内容添加到数组 a 的内容的超级简单方法时遇到问题。这是代码。

method addAssign(a: array<real>, b: array<real>)
   requires a != null && b != null && a.Length == b.Length;
   modifies a
   ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + b[k];
{
   var i := 0;
   assert a == old(a);
   while(i < a.Length)
      invariant 0 <= i <= a.Length
      invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k])
      invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + b[k];
   {
      assert a[i] == old(a[i]); // dafny verifies this
      a[i] := a[i] + b[i];
      assert a[i] == old(a[i]) + b[i]; // dafny says this is an assertion violation
      i := i + 1;
   }
}

Answer 1

（我删除了我的第一个答案，因为它不起作用）。

问题似乎在于 Dafny 检测到了潜在的混叠问题。作为一个实验，我首先修改了你的代码以获得一个更简单的函数来验证：

method addOne(a: array<real>)
   requires a != null;
   modifies a;
   ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + 1.0;
{
   var i := 0;
   assert a == old(a);
   while(i < a.Length)
      invariant 0 <= i <= a.Length
      invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k])
      invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + 1.0;
   {
      assert a[i] == old(a[i]); // dafny verifies this
      a[i] := a[i] + 1.0;
      assert a[i] == old(a[i]) + 1.0; // dafny *doesn't* say this is an assertion violation
      i := i + 1;
   }
}

唯一的区别是我使用的是文字实数 (1.0) 而不是从b 提取的实数。为什么那会有所作为？

假设您使用看起来像

的调用来调用您的方法

addAssign(a,a)

那么在函数体中b 和a 都引用同一个数组。例如，假设a[0] 是 1.0。然后在第一次循环中执行a[0] := a[0] + b[0]。

这会将 a[0] 设置为 2.0。但是——它也将b[0] 设置为2.0。

但在这种情况下assert a[0] == old(a[0]) + b[0]相当于

assert 2.0 == 1.0 + 2.0 -- 应该失败。

顺便说一句——以下确实验证：

method addAssign(a: array<real>, b: array<real>)
   requires a != null && b != null && a.Length == b.Length;
   modifies a;
   ensures forall k:: 0 <= k < a.Length ==> a[k] == old(a[k]) + old(b[k]);
{
   var i := 0;
   assert a == old(a);
   while(i < a.Length)
      invariant 0 <= i <= a.Length
      invariant forall k:: i <= k < a.Length ==> a[k] == old(a[k])
      invariant forall k:: 0 <= k < i ==> a[k] == old(a[k]) + old(b[k]);
   {
      assert a[i] == old(a[i]); // dafny verifies this
      a[i] := a[i] + b[i];
      assert a[i] == old(a[i]) + old(b[i]); // and also this!
      i := i + 1;
   }
}