arrays - 在 SPARK 检查数组元素报告“数组索引检查可能失败”中设置先决条件

Question

继续我从 Dafny 转录到 SPARK 的努力，我遇到了为数组创建先决条件的问题，该数组应该在调用函数时进行排序：

type Integer_Array is array (Positive range <>) of Integer;
function BinarySearch(a : Integer_Array; key: Integer) return Integer
  with
    --      requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j] // a is a sorted array
    Pre => ((a'Length >= 2) and then (for all i in 1 .. a'Length - 1 => a(i-1) < a(i)))
--                                                                        |        ^---- array index check might fail
--                                                                        \------------- array index check might fail

我错过了什么？

Answer 1

(i-1)绝对可以超出范围。例如，对于索引从 1 到 5 的数组，将为 0。我认为使用and而不是i-1会更好：'First'Last'Range

for all i in a'First + 1 .. a'Last => a(i-1) < a(i)

通常最好避免在 Ada 的循环中使用数字作为索引。该数组可以从各种值开始，例如 3 到 6，而不仅仅是 1。