SPARK编写数组校验前置条件提示‘数组索引检查可能失败’问题

你触发索引检查报错的核心原因是没有适配SPARK/Ada的数组下标规则，踩了两个逻辑漏洞：

• 你定义的Integer_Array下标类型为Positive，该类型的合法取值最小为1，你在前置条件中写的a(i-1)在循环变量i取起始值1时会得到下标0，属于完全非法的数组索引
• 你硬套了Dafny默认0基数组的写法，没有使用SPARK数组内置的下标边界属性，就算你规避了0下标问题，只要数组不是从1开始计数（比如自定义下标从5开始的数组），你的写法依然会触发索引错误

SPARK中数组的排序前置条件不要硬编码下标范围，应当使用数组的'First（数组第一个元素的下标）、'Last（数组最后一个元素的下标）属性编写通用逻辑，不需要额外增加a'Length >=2的判断：当数组长度小于2时，a'First .. a'Last -1是个空区间，for all量化判断在空区间上默认成立，天然符合长度为0/1的数组本身就是有序的逻辑。

修正后的代码如下：

type Integer_Array is array (Positive range <>) of Integer;
function BinarySearch(a : Integer_Array; key: Integer) return Integer
  with
    -- 非严格升序用<=，严格升序用<即可
    Pre => (for all i in a'First .. a'Last - 1 => a(i) < a(i + 1));

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