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来解决此问题。

Answer 2

我为Dafny项目编写了您的示例，以及我们如何使用代码操作来解决它：https://github.com/dafny-lang/dafny/issues/3102

我在这里复制详细的解决方案来计算一个最弱的先决条件。

---

明确断言将导致

{
c[j] := a[h] + b[i];
assert c[j] == a[h] + b[i];
}

现在，我们不能仅仅"；向上移动断言"；，因为我们必须在赋值后对堆的状态进行推理，而old@还不能引用后面定义的标签。因此，下一步将是引入标签，并在分配下面进行最弱的先决条件计算

{
label before: // Added
c[j] := a[h] + b[i];
assert old@before(a[h] + b[i]) == a[h] + b[i]; // Added, now failing
assert c[j] == a[h] + b[i];
}

这方面的好处是它将帮助用户发现"；旧的"；语法自然。因为最弱的先决条件现在看到了另外两个潜在冲突的引用，所以它可以建议以下代码操作来在赋值后删除对堆的引用：

{
label before: // Added
c[j] := a[h] + b[i];
assert old@before(a[h] + b[i]) == (if a == c && j == h then old@before(a[h] + b[i]) else a[h]) + (if b == c && j == i then old@before(a[h] + b[i]) else b[i]); 
assert c[j] == a[h] + b[i];
}

现在，因为这个表达式在赋值c[j}之后根本不引用堆，所以最弱的前置条件演算将能够在old@表达式之前移动这个断言并移除它。

{
assert a[h] + b[i] == (if a == c && j == h then a[h] + b[i] else a[h]) + (if b == c && j == i then a[h] + b[i] else b[i]); // Just added, now failing.
label before:
c[j] := a[h] + b[i];
assert old@before(a[h] + b[i]) == (if a == c && j == h then old@before(a[h] + b[i]) else a[h]) + (if b == c && j == i then old@before(a[h] + b[i]) else b[i]); 
assert old@before(a[h] + b[i]) == a[h] + b[i];
assert c[j] == a[h] + b[i];
}

并最终将其移动到该方法的需求。然后，用户可以细化这个最弱的前提条件，以便他们只保留a != c && b != c(如果他们愿意的话)。

Answer 3

我也添加了另一个答案，因为我认为它是独立的。默认情况下，postcondition指的是方法末尾的堆。您可以通过引用堆开头的a和b的取消引用，插入old(...)，使后条件保持不变，如下所示：

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] == old(a[h] + b[i])
{
c[j] := a[h] + b[i];
}

这就像一种魅力，正是你的方法所做的。感谢Rustan Leino为我指出了这个解决方案。