1

私はJMLでそれをしたい:

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

私はそれを機能させることができませんでした.JML仕様で多くの例を見ましたが、それを行う方法を見つけることができませんでした.

では、どうすれば作れますか？

4

1 に答える 1