java - OpenJML 中的编程静态检查

Question

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

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

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

Answer 1

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

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

为了验证(又名“静态检查”)，您可以查看当前 source distribution 中的“key.core.example”包这应该让你开始。

据我所知，OpenJML 和 KeY 是目前唯一积极维护的用于静态检查 JML 注释的工具。还有其他的，比如 ESC/Java2 和 KRAKATOA，但它们似乎已经过时了。 Key 得到积极维护，但是 does not cover all of the Java language对比OpenJML(以后可能会有LLVM或者bytecode的版本，既然有相应的规划，那么情况可能会有所改善)。