1

我想在 JML 中做到这一点:

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

我无法使其工作,在 JML 规范中看到了很多示例,但找不到如何做到这一点的方法。

那么,我该怎么做呢?

4

1 回答 1

1

一种方法是使用暗示“防范”无意义的数组值:

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

使用更新的语法 for \forall,我相信你也可以这样写:

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

(i >= 0 && i < array.length-1)范围表达式在哪里。

于 2011-03-23T04:35:02.180 回答