JML: Cómo especificar un requisito de una matriz con los elementos de media luna?

Question

Quiero hacer eso en JML:

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

No podía hacer que funcione, vio una gran cantidad de ejemplos en las especificaciones JML, pero no pudo encontrar una manera de cómo hacerlo.

Así que, ¿cómo puedo hacerlo?

Answer 1

Una forma es "protector" contra valores de la matriz sin sentido usando implicación:

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

Con la nueva sintaxis para \forall, creo que también se puede escribir:

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

donde (i >= 0 && i < array.length-1) es la expresión gama.