gpt4 book ai didi

java - JML:如何指定具有新月形元素的数组的要求?

转载 作者:太空宇宙 更新时间:2023-11-04 08:48:05 25 4
gpt4 key购买 nike

我想在 JML 中执行此操作:

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

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

那么,我怎样才能做到呢?

最佳答案

一种方法是使用蕴涵来“防范”无意义的数组值:

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

关于java - JML:如何指定具有新月形元素的数组的要求?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/3946545/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com