问题标签 [openjml]

I am experimenting with OpenJML in combination with Z3, and I'm trying to reason about double or float values:

I have already found out OpenJML uses AUFLIA as the default logic, which doesn't support reals. I am now using AUFNIRA.

Unfortunately, the tool is unable to prove this class:

Why is this?

我有一个类，其矩阵在特定位置初始化为所有 0 和 1：

我想添加一个不变量来检查我是否总是只有一个值为 1 的 1 单元格和值为 0 的 35 个单元格。我尝试这样做：

但它在构造函数之后给了我不变的错误。我如何遍历矩阵来检查属性？

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

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

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

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

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

我正在 IJ 中开发 Java 代码库，目前正在使用 Maven 构建。我想用某种形式的合同来补充一些代码，这些合同将在 Maven 构建中获得。到目前为止，我一直没有成功寻找这种现成的功能：

• OpenJML，但这似乎需要它自己的工具来分析您的代码，我找不到将其轻松集成到构建中的方法。
• Jetbrains 合同。这些将通过检查在 IntelliJ 中发出警告，但它们不会影响构建。

注意：我只关心编译时可检查的合约。我有 JUnit 来处理运行时方面的问题。

执行合同：

我添加了这一部分来回答询问我想要执行什么样的合同的评论。理想情况下，我想要最强大的解决方案，条件是该解决方案是完整的。当我在这里说完整时，我的意思是一种合同语言和一个合同检查器，这样语言中的每条语句都可以在编译时由检查器检查为好/坏。我知道这可能是一个很大的问题，但即使是最简单的合同，例如Jetbrains 提供的合同，我也会感到满意。

对于一个具体的例子，考虑这个函数：

这成功通过了 Jetbrains 合约：

并未能完成这个人为的合同：

但是有了上述人为的、糟糕的合同，Maven 构建仍然可以正常工作。构建不会获取检查结果 - 这些仅在 IJ 内可见。如果违反任何合同，我希望能够参与构建并失败。

我正在尝试静态检查 Java 我的代码。唯一的问题是它使用 android sdk 并且 OpenJML 无法识别 android 类。例如，这是我得到的日志的一部分：

有没有办法将 OpenJML 与 android SDK “链接”？或者也许还有其他一些与android兼容的工具？也许 Jessie/Krakatoa 可以做到？

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，而我的项目使用它需要的任何东西吗？

When I run my code with the OpenJML test in eclipse. I get this output ......

Skipping long-running tests 5 system specification classes found for esc testing JRE version 1.8.0_202 5 system specification classes found for rac testing TEST: testParseAndCheckCrash

TEST: testParseAndCheckCrash2

java.lang.NullPointerException java.lang.NullPointerException at org.eclipse.core.internal.runtime.InternalPlatform.getBundles(InternalPlatform.java:231) at org.eclipse.core.internal.runtime.InternalPlatform.getBundle(InternalPlatform.java:221) at org.eclipse.core.runtime.Platform.getBundle(Platform.java:1424) at org.jmlspecs.openjml.JmlSpecs.appendInternalSpecs(JmlSpecs.java:351) at org.jmlspecs.openjml.JmlSpecs.setSpecsPath(JmlSpecs.java:459) at org.jmlspecs.openjml.JmlSpecs.setSpecsPath(JmlSpecs.java:415) at org.jmlspecs.openjml.JmlSpecs.initializeSpecsPath(JmlSpecs.java:273) at org.jmlspecs.openjml.Main.setupOptions(Main.java:962) at org.jmlspecs.openjml.Main.processArgs(Main.java:1017)

What am I doing wrong, I am looking for the test to tell me what is wrong with my code and which line.

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

代码 ：

JML 警告：

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

谢谢您的帮助

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

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

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

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