Making a precondition in SPARK checking array element reports 'array index check might fail&#03-CodePudding

Continuing my efforts transcribing from Dafny to SPARK I run into problems making a precondition for an array that should be sorted on invoking the function:

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

What have I missed?

CodePudding user response：

(i-1) definitely can be out of scope. For example, for an array indexed from 1 to 5, i-1 will be 0. I think it would be better if you use 'First and 'Last instead of 'Range:

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

Generally it is a good idea to avoid use numbers as indexes in loops in Ada. That array can start from various values, like 3 to 6, not just 1.