Dafny数组元素包含断言触发违反：为何出现该问题？

先把你的测试方法代码贴出来方便分析：

method test() { 
  var a := new int[5]; 
  a[0] := 1; a[1] := 1; a[2] := 2; a[3] := 3; a[4] := 3; 
  var b := new int[3]; 
  b[0] := 1; b[1] := 2; b[2] := 3; 
  assert(forall i :: exists j :: ((0 <= i < 5) && (0 <= j < 3)) ==> (a[i] == b[j])); 
}

这个断言失败的核心原因有两个，都是逻辑结构和数组访问合法性的问题：

• 量词作用域未限制，导致非法数组访问
  你写的forall i没有限定i的取值范围，意味着这个量词会覆盖所有整数（不只是数组a的合法索引0-4）。当i取5、-1这类超出a索引范围的值时，表达式a[i]属于数组越界访问——在形式化验证工具（比如Dafny）中，这种访问是未定义行为，工具无法保证该表达式的合法性，因此直接判定断言不成立。

• 蕴含式位置错误，语义完全偏离预期
  你原本想验证的应该是：数组a里的每一个合法元素，都能在数组b中找到对应的值。正确的逻辑结构应该是先限定i的合法范围，再对每个合法i断言存在对应的j：

  assert(forall i :: (0 <= i < 5) ==> exists j :: (0 <= j < 3) && (a[i] == b[j]));
  

  而原断言把i和j的范围都塞进了蕴含式的前件，变成了：对于所有整数i，存在某个整数j，使得如果i是a的合法索引且j是b的合法索引，那么a[i]等于b[j]。这个语义不仅包含了越界访问的非法情况，还把原本的“限定范围后断言相等”变成了“条件成立时才需要相等”，完全偏离了你想要验证的逻辑。

简单来说，原断言既没限制i的范围导致非法访问，又写错了逻辑结构，所以工具会返回断言违反。

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