JML: How to specify a requirement of an array with crescent elements?

Question

I want to do that in JML:

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

I couldn't make it work, saw a lot of examples in JML specs, but couldn't find a way how to do it.

So, how can i make it?

Answer 1

One way is to "guard" against nonsense array values using implication:

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

With the newer syntax for \forall, I believe you could also write:

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

where (i >= 0 && i < array.length-1) is the range expression.