OpenJML 中的程序化静态检查

Question

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

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

有人知道一个简单的例子吗？

Answer 1

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

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

对于验证（也称为“静态检查”），您可以查看当前 source distribution 中的“key.core.example”包，这应该可以帮助您入门。

据我所知，OpenJML 和 KeyY 是目前唯一积极维护的用于静态检查 JML 注释的工具。还有其他的，例如 ESC/Java2 和 KRAKATOA，但它们似乎已经过时了。 Key是积极维护的，但是does not cover all of the Java language对比OpenJML（以后可能会有LLVM或者字节码版本，既然有相应的计划，那情况可能会好转）。