OpenJML中的编程静态检查

Question

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

不幸的是，静态检查的手动输入(第5.2.4节)是空的，并且似乎没有给出具体的示例。

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

Answer 1

不幸的是，我无法帮助您解决OpenJML问题，即使在新版本的手册中，您提到的部分也是空的。

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

对于验证(也称为“静态检查”)，您可以查看当前source distribution中的"key.core.example“包，这将使您开始使用。

据我所知，OpenJML和KeY是目前唯一积极维护的静态检查JML注解的工具。还有其他的，比如ESC/Java2和KRAKATOA，但它们似乎已经过时了。KeY是积极维护的，但does not cover all of the Java language与OpenJML不同(也许将来会有LLVM或字节码版本，因为有相应的计划，那么情况可能会改善)。