问题标签 [openjml]

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

和产生的输出：

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

我有以下代码：

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

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

我想在另一个方法的后置条件（和循环不变量）中调用一个类方法。我发现最相关的是StackOverflow 中的这篇文章。

我试图打开那里提供的链接（http://www.ibm.com/developerworks/java/library/j-jml/index.html）；但是，它不再起作用了。1-是否有任何（其他）资源可以找到“如何在其他函数的后置条件中调用类方法”？

2- 一旦我尝试在 OpenJML 中测试该示例，我收到静态验证错误：

在此处输入图像描述

只是我能够对这个例子使用运行时断言检查：

在此处输入图像描述

关于在静态验证（或运行时断言）中调用后置条件中的方法的任何帮助将不胜感激。谢谢

-- 我在 ubuntu 20.04 上使用 openjml 0.17.0-alpha-9。