问题标签 [jml]

我正在使用 java 开发一个简单的 msn 客户端，但我不知道如何使用 JML 库设置 http 代理参数。显然它不是图书馆原生的=/

我正在使用 JML 来测试一些简单的类。我有类 Interval.java 、 SequenceInterval.java 和 TestSequence.java，都在同一个包（默认包）中。当我尝试使用 jmlc 编译 SequenceInterval 时，它显示相同的错误：

每一行我都使用一个 Interval 类型的对象。这是我第一次使用 ESCJava 和 JML，所以我完全是新手。我忘了smth吗？我阅读了有关“模型导入”注释的信息，但这不是我所需要的，因为我在 Java 代码中使用了类 Interval。那么，我该如何摆脱这个错误呢？这显然不是类路径的问题。肿瘤坏死因子

我正在寻找一个用 Java 编写的能够读取 JML 的解析器。

基本上我希望解析器能够读取 JML 块并知道它属于哪个方法。

我一直在看 OpenJML 项目，但只是项目设置太多了。

我试图证明我的收藏中是否存在具有特定状态的对象。我的集合由具有名为 getStatus() 的方法的对象组成。现在我想证明这个集合中是否存在具有给定状态的对象。

问题是 orders[i] 必须是数组类型，它是 JMLObjectSequence 类型。有没有办法将此序列转换为数组，语法如何？

另一种方法是（使用 itemAt(i)）：

但是 itemAt(i) 返回一个不是 Order 类型的 Object - 所以找不到方法 getStatus()。

我会很高兴得到一些帮助。那里没有太多的例子。

类方法的 JML 后置条件是否可以包含对另一个方法调用的调用

例如我有这个类：

对于 doB 的后置条件，我可以有：ensures doA(x) = doA(y)？

当我尝试从http://jmlspecs.sourceforge.net/openjml-updatesite的更新站点安装 openJML 插件时，出现以下错误：

我尝试安装以前版本的插件，但都导致类似的“找不到工件”错误。任何人都知道为什么这不起作用？或者有一个我可以用来让 Eclipse 插件工作的解决方法？

提前致谢！

我正在学习软件工程课程，在那里我看到了 JML 的用法。这是一段示例代码：

它说正式的 JML 规范是可执行的！

我的问题是，当我们使用 f=-4 调用这个 sqrt 函数时，这段代码是否给出错误或抛出异常或给出任何警告？我在我的电脑上试了一下，效果很好，打印出-2。那么JML可执行是什么意思呢？为什么我们不只使用评论来做到这一点？谁能解释一下？

谢谢

我们如何将 JML 应用于 Java 代码？我仍然是合同设计的新手，并且对如何将其应用到程序中非常迷茫。

http://jmlspecs.sourceforge.net/

使用：

• 开放式JML
• 网豆 7.3
• Java SDK 1.7

我已经将 OpenJML jar 文件添加到 Netbeans 的类路径中。我尝试了 cofoga google jml 版本，您只需在其中导入 com.google.java.contract.Ensures；import com.google.java.contract.Requires 然后你可以添加前置条件和后置条件

我们如何在我的程序中使用 openJML 指定前置条件和后置条件？

我正在尝试安装 JML 并在尝试各种 eclipse 发行版后成功，但出现此错误：（使用 eclipse-java-indigo-SR2-win32）当我使用菜单时出现错误：JML > Static Check (ESC)

未指定证明者的可执行文件 - 使用 -exec 或定义 openjml.prover 请提供一些帮助

图片链接

我有一堂课Edge.java。当我通过 OpenJML 运行它时，会发生这种情况：

error: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can. Reason: com.sun.tools.javac.code.Symbol$TypeSymbol cannot be cast to com.sun.tools.javac.code.Symbol$ClassSymbol

奇怪的是，我什至还没有开始输入 jml 符号。

我的 jdk 是 1.7，openjml 是最新的（重新下载以确保）。

这是用于运行 openjml 的命令（按照站点中的示例）： java -jar "E:\Downloads\openjml\openjml.jar" -esc -prover z3_4_3 -exec "E:\Downloads\z3-4.3.0-x64\bin\z3.exe" -noPurityCheck Test.java

编辑：我可以确认，即使是一个非常简单的泛型类也会导致这个错误：

Edge.java