2

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?

Andreas
  • 5,086
  • 3
  • 16
  • 36

1 Answers1

3

(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.

thindil
  • 881
  • 5
  • 9
  • 1
    Totally forgot about alternate index ranges, thanks. – Andreas Oct 10 '21 at 11:27
  • 1
    FYI, `a'Length >= 2` is required to avoid overflow issues on `a'First + 1` :-) – Andreas Oct 10 '21 at 12:27
  • 1
    @Andreas About forgetting, not a problem, this is why we have SPARK to check and Stack Overflow to decrypt its messages. And this `a'Length` is a nice catch. :) – thindil Oct 10 '21 at 16:40