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]))

where (i >= 0 && i < array.length-1) 是范围表达式。