arrays - Dafny:验证最简单的数组求和是行不通的。有人可以向我解释为什么吗？

Question

当我有三个数组并且 c[j] := b[h] + a[i] 时。验证 c[j] == b[h] + a[i] 不起作用。有人可以解释一下为什么吗？确保所有索引都在范围内，并且所有三个数组都是 int 数组。这是我的代码:

method addThreeArrays(a: array<int>, b: array<int>, c: array<int>, h: int, i: int, j: int)
  modifies c
  requires 0 <= h < a.Length
  requires 0 <= i < b.Length
  requires 0 <= j < c.Length
  
  ensures c[j] == a[h] + b[i]
  {
    c[j] := a[h] + b[i];
  }

我希望“确保”这一行是正确的。但是 Dafny 给出了错误。 “后置条件”可能不成立。我只想了解我的错误在哪里。感谢你们! :)

Answer 1

由于 Dafny 数组是在堆上分配的，因此它们可以使用别名。因此可以调用您的方法，例如，c 和 a 指向内存中的同一个数组。此外，j == h 也是可能的。在这种情况下，后置条件可能不成立，因为写入 c[j] 也会写入 a[h](因为 c 和 a 指向同一个数组和 j == h)。

您可以通过添加前提条件 a != c 和 b != c 来解决此问题。