JML: Как указать требование массива с полумесяцами?

Question

Я хочу сделать это в JML:

//@ requires (\forall int i : array[i] < array[i+1])
void calculatesDistances(int[] array){
 ..
}

Я не мог заставить это работать, видел много примеров в спецификациях JML, но не мог найти способ, как это сделать.

Итак, как я могу это сделать?

Answer 1

Одним из способов является "защита" от бессмысленных значений массива с помощью импликации:

  (\forall int i; (i >= 0 && i < array.length-1) ==> (array[i] < array[i+1]))

С новым синтаксисом для \forallЯ полагаю, вы также можете написать:

  (\forall int i; (i >= 0 && i < array.length-1) ; (array[i] < array[i+1]))

где (i >= 0 && i < array.length-1) это выражение диапазона.