The manual for OpenJML (http://jmlspecs.sourceforge.net/OpenJMLUserGuide.pdf) intimates that static-checking of Java compilation units can be done programmatically.
Unfortunately, the manual entry for static-checking (Section 5.2.4) is empty, and no specific examples appear to be given for this.
Does anyone know of a simple example?
Unfortunately I cannot help you out for OpenJML, even in the new version of the manual, the section you refer to is empty.
However, you could try other tools such as the KeY program verifier with which you can statically prove your JML annotations correct, either using KeY as a front-end or also programmatically as a back-end. The code at the page referred to, which presents the programmatic usage of the symbolic execution API of KeY may be look quite intimidating at the first glance, but it contains a lot of boilerplate which you might actually not need because the available all options are explained.
For verification (aka "static checking"), you could look into the "key.core.example" package in the current source distribution which should get you started.
As for my knowledge, OpenJML and KeY are the currently only actively maintained tools for statically checking JML annotations. There were others, such as ESC/Java2 and KRAKATOA, but they seem to be outdated. KeY is actively maintained, but does not cover all of the Java language in contrast to OpenJML (maybe there will be LLVM or bytecode versions in the future, since there are corresponding plans, then the situation might improve).
