问题标签 [jml]

我需要一种用于 JML 的排序方法我尝试过插入排序，但我不知道我需要什么，并确保或维护我需要什么。请帮忙。我需要//@requires、//@ensures 和//@maintaining。

目前，我正在尝试使用 Java 程序的Key工具进行一些形式验证。

这是我的带注释的 Java 代码：

令我惊讶的是 Key，它无法证明当前程序根据其规范是有效的。Key在目标 54 失败。当前目标窗口显示：

我不太明白：未能证明规范的主要原因是什么？

OpenJML 可作为 Eclipse 插件（安装站点 http://jmlspecs.sourceforge.net/openjml-updatesite）使用，它似乎可以在 Eclipse Photon 中安装。

但是文档说它只能在 OpenJDK 1.8 上运行，并且不能是任何其他 JDK（比如 Oracle JDK）。它也不能是不同于 1.8（比如 1.9）的（OpenJDK）版本。

我在 Eclipse 中的项目都使用 (Oracle) JDK，此外我们很快计划从 JDK 1.8 升级到 1.9。

我可以设置 OpenJML 以便它使用它想要的 OpenJDK 1.8，而我的项目使用它需要的任何东西吗？

如何验证 JML 工具（如 OpenJML）中的相交、联合和差异等基本集合操作，其中不支持“\intersect \set_minus \set_union”等关键字？

我要对其进行验证的 Java 接口如下所示：

我刚开始使用 OpenJML，这里是我的代码和我的 JML 警告：

代码 ：

JML 警告：

我不明白为什么无法建立特殊的后置条件。

谢谢您的帮助

我很想更好地理解 Java 密钥证明的限制。我想出了一个特定的数组元素将触发空指针异常的场景。当我通过证明程序运行它时，它通过了。知道这是为什么吗？它应该会失败，因为将在数组元素 86454 处抛出空指针。请注意“normal_behaviour”意味着它应该无异常终止。

我尝试安装 Java 建模语言 (JML)，但出现了问题。我使用 Eclipse IDE，Windows 10。我打开了 Eclipse -> 帮助 -> 安装新软件，然后我使用它安装了

然后，我重新启动 Eclipse，新图标出现在顶部菜单栏中。当我尝试编译或使用 JML 图标时，Eclipse 显示了一个巨大的错误消息。（图片）

我能做些什么来解决这个问题？我在网站上没有找到解决方案

我得到了一项任务，我必须删除 JML 产生的每个警告。
如果我在构造函数 my 中调用一个方法requires并且ensures不再验证，尽管为被调用函数添加了相同的约束。
我被要求仅使用requires,ensures和。 这是代码：invariantloop_invariant

和产生的输出：

一种解决方案是使函数arraycopy非静态，但我不明白为什么。

我有以下代码：

我在其中插入了一些 OpenJML 注释。当我在 therminal 上运行 OpenJML 时，我收到以下错误：

我真的不明白为什么\forall循环和//@ assert i >= 0;断言不起作用。他们在我看来还不错。

我对 java 有点陌生，所以在编程时我注意到我必须为我的子例程提供 JML 注释。当我使用面向对象编程时，我注意到接口的使用，并且我必须使用 JML 规范声明方法，问题是，当我完成接口之后，我现在在类中实现方法实现接口，当我再次声明该类时，我是否也应该再次在该类上方指定 JML 规范，还是可以将其省略，因为它位于接口中？