Dafny中数组赋值后置条件验证失败原因咨询

Dafny提示后置条件不成立，核心原因是它检测到了一种数组别名+索引重叠的反例场景：

• 当数组c和a指向同一个内存地址（别名），且索引h等于j时，执行赋值操作c[j] := a[h] + b[i]会同时修改a[h]的值。
• 此时后置条件中的a[h]是修改后的新值，导致等式c[j] == a[h] + b[i]必然不成立。

举个具体的反例：假设a和c是同一数组，h=j=0，b[i]=5，初始a[0]=3。赋值后c[0]（即a[0]）变为8，后置条件检查8 == 8 +5，显然不成立。

你可以根据实际需求选择以下两种方案：

方案1：排除冲突场景 #

在requires子句中添加条件，禁止数组别名或索引重叠：

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
  // 禁止c与a、b别名
  requires c != a
  requires c != b
  // 或者单独禁止h与j重叠（如果允许别名但索引不重叠的话）
  // requires h != j
  
  ensures c[j] == a[h] + b[i]
  {
    c[j] := a[h] + b[i];
  }

方案2：引用初始值 #

如果需要允许数组别名的情况，用old关键字引用方法执行前的a[h]和b[i]值，确保后置条件对比的是赋值时使用的原始数值：

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
  
  // 使用old关键字获取方法开始时的a[h]和b[i]值
  ensures c[j] == old(a[h]) + old(b[i])
  {
    c[j] := a[h] + b[i];
  }

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