Создание предварительного условия в 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, i-1будет 0. Я думаю, было бы лучше, если бы вы использовали 'Firstа также 'Lastвместо 'Range:

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

Как правило, рекомендуется избегать использования чисел в качестве индексов в циклах Ады. Этот массив может начинаться с различных значений, например, от 3 до 6, а не только с 1.