java - OpenJML 中的程序化静态检查

Question

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

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

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

Answer 1

不幸的是，我无法为您提供 OpenJML 的帮助，即使在新版本的手册中，您所指的部分也是空的。

但是，您可以尝试使用其他工具，例如KeyY 程序验证器，使用它可以静态地证明您的 JML 注释正确，或者使用 KeyY 作为前端，或者也以编程方式作为后端。所引用页面上的代码，它展示了 Key 的符号执行 API 的编程用法，乍一看可能看起来很吓人，但它包含很多你可能实际上不需要的样板文件，因为解释了所有可用的选项.

对于验证（又名“静态检查”），您可以查看当前源代码分发中的“key.core.example”包，这应该可以帮助您入门。

据我所知，OpenJML 和 KeyY 是目前唯一积极维护的静态检查 JML 注释的工具。还有其他的，例如 ESC/Java2 和 KRAKATOA，但它们似乎已经过时了。Key 是积极维护的，但相对于 OpenJML并没有涵盖所有的 Java 语言（未来可能会有 LLVM 或字节码版本，因为有相应的计划，那么情况可能会有所改善）。