javaspecificationsjml

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

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?

Solution

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