JML：如何指定具有新月元素的數組的要求？

Question

我想要做的是，在JML：

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

我不能讓它工作，看到了很多的JML規範的例子，但未能找到一種方法如何做到這一點。

那麼，我該怎麼做呢？

Answer 1

一種方法是用寓意爲「守衛」反對瞎說陣列值：

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

隨着\forall較新的語法，我相信你也可以這樣寫：

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

其中(i >= 0 && i < array.length-1)是範圍表達。