JML: Comment spécifier une exigence d'un tableau avec des éléments en croissant?

Question

Je veux faire en JML:

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

Je ne pouvais pas le faire fonctionner, a vu beaucoup d'exemples dans les spécifications JML, mais n'a pas pu trouver un moyen comment le faire.

Alors, comment puis-je le faire?

Answer 1

Une façon est de « garde » contre les valeurs de tableau non-sens en utilisant l'implication:

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

Avec la nouvelle syntaxe pour \forall, je crois que vous pouvez aussi écrire:

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

où (i >= 0 && i < array.length-1) est le expression de gamme.