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) 是范围表达式。