为何Dafny能验证全负数组的存在量词断言，却无法验证含正元素的？

这是Dafny自动定理证明器的启发式搜索逻辑导致的：

• 第一个代码示例中，数组的两个元素都是负数。不管选择k=0还是k=1，都能满足0 <= k < arr.Length && arr[k] < 0的条件。Dafny的证明器不需要额外提示，就能轻松找到符合要求的k实例，因此断言直接通过验证。

• 第二个代码示例中，只有k=0满足条件，但Dafny默认的启发式搜索不会自动遍历所有可能的索引值来寻找实例。证明器需要更明确的引导才能定位到这个唯一符合条件的k。

解决方法 #

你可以通过添加辅助断言来给证明器提供线索，比如：

var arr := new int[2];
arr[0], arr[1] := -1, 2;
assert arr[0] < 0; // 先确认索引0的元素满足条件
assert exists k :: 0 <= k < arr.Length && arr[k] < 0;

或者直接在存在量词中指定候选实例的特征，缩小证明器的搜索范围：

var arr := new int[2];
arr[0], arr[1] := -1, 2;
assert exists k :: 0 <= k < arr.Length && k == 0 && arr[k] < 0;

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