JML: How to specify a requirement of an array with crescent elements?
-
08-10-2019 - |
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?
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.
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow