OpenJML（http://jmlspecs.sourceforge.net/OpenJMLUserGuide.pdf）手册提示可以以编程方式对Java编译单元进行静态检查。
遗憾的是，用于静态检查的手动输入（第5.2.4节）为空，并且为此没有给出具体的示例。
有人知道一个简单的例子吗？
最佳答案
不幸的是，即使在新版本的手册中，您引用的部分为空，我也无法为您提供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或字节码版本，因为有相应的计划，所以情况可能会有所改善）。