问题标签 [jml]

我已经为 Eclipse 安装了 OpenJML 工具 ( http://openjml.org/ ) 并且正在使用它，而且效果很好。

但是，现在我需要从命令行调用jmlc和jmlunit工具。从网上搜索看，这些工具应该在JML的某个目录下，我应该把它们添加到PATH中，调用相应的命令就可以正常使用了。但是一旦我下载了 OpenJML，我就只有 3 个 jar 文件并且根本没有目录。此外，在 JML 官方页面上，除了 OpenJML 之外，没有其他链接可以下载其他版本。在我看来，我没有得到明显的东西。

所以，问题是我如何找到这些工具来在命令行上运行它们？

提前致谢。

OpenJML 手册 ( http://jmlspecs.sourceforge.net/OpenJMLUserGuide.pdf ) 暗示可以通过编程方式对 Java 编译单元进行静态检查。

不幸的是，静态检查的手动条目（第 5.2.4 节）是空的，并且似乎没有为此给出具体示例。

有谁知道一个简单的例子？

我最近在一次旧考试中阅读了以下 JML 代码：

我不明白

部分。是什么a[*]意思？如果只有

?

（参考链接会很棒。）

The statement after decreases has to get strictly smaller in each loop and always be non-zero. But does it have to reach 0? Does it have to get smaller by one?

在我的类 Test 中，我有一个名为 a 的五个 int 数组，以及将一个添加到所选单元格的方法 addOne(int index)。我在 JML 中编写了一个简单的前提条件来控制传递给方法的索引。然后我尝试违反此先决条件，使用负索引调用该方法，而 JML 无法捕获此错误。怎么了？

这是测试类：

这是主要的：

抛出异常：java.lang.ArrayIndexOutOfBoundsException：-2。

使用任何 JML 消息。

我是一名助教，为我的学生准备作业，以便他们学习 JML 和合同设计。我给他们 3 个文件：RArray.refines-java（带有空白 JML 断言的规范）、RArray.java（实现先前规范的类）和TestRArray.java（测试类）。

为了执行这项工作，他们必须计算 3 个命令：

1. jmlc RArray.refines-java（规范和实现的编译）
2. javac TestRArray.java（测试类的编译）
3. jmlrac TestRArray（使用 jml 运行时断言检查器进行验证）

然而，为了做到这一点，他们必须在学校的计算机上安装 JML，显然没有人拥有 root 访问权限。我尝试先安装它，它似乎不需要任何 root 访问权限 - 我按照这个法语教程，使用这个zip 文件。

我在我的 ubuntu 14.04 笔记本电脑上试过，它工作得很好，我已经能够为作业管理一些结果。即使在学校，在 Fedora 上，我也可以毫无怨言地安装这些工具，并将它们添加到 PATH。但是，在学校，我运行时遇到错误 jmlc RArray.refines-java。

这是我的错误：

我之前尝试过搜索，看来这可能是重复的 CLASSPATH 或这些行中的某些问题，但我无法访问它。

我还尝试再次下载 ZIP 文件，以验证这个格式错误的类是否会被修复，但没有运气。

我尝试运行javac RArray.refines-java，它按预期进行编译，因此它一定是 jml 问题。

这是结果java -version：

这是结果jml -version：

您对如何解决此问题有任何想法吗？我希望我不必丢弃所有东西。

我正在研究为 java.util.PriorityQueue.remove(Object object) 方法创建 JML 规范。到目前为止，我已经想到了以下前提：

我现在正试图找出后置条件。那么这个方法的 Ensure 字段是什么？我觉得它应该涉及 size() 方法并确保数据不再在队列中，但我不确定如何编写。

有人可以对 Java 建模语言中的以下不变量给出准确的含义，指出它们之间的主要区别吗？

• 公共不变量
• 抽象函数（私有不变量）
• 表示不变量（私有不变量）

我正在为我的项目使用 OpenJML 插件，但 Eclipse 自动格式化与我的 JML 代码混淆。JML 写在//@符号之后。

然而，Eclipse 自动格式化在//和@符号之间添加了一个空格，使我的 JML 代码无用。

有没有一种方法可以禁用在//和@符号之间添加空格，或者有一种方法可以完全禁用注释后的空格？

我尝试更改格式化程序配置文件，但在那里找不到设置。

我也尝试过自动删除尾随空格，如下所述：如何在 Eclipse 中自动删除尾随空格？但这也没有用。我假设是因为我专门尝试更改评论自动格式。

我需要一种用于 JML 的排序方法，我尝试了冒泡排序，但我不知道我需要什么，并确保或维护我需要什么。我是这种语言的新手。