OpenJML Examples

The following links show various working or tutorial examples of Java programs with OpenJML annotations, enabling the OpenJML tool to prove correctness or to point out errors. Additional examples are part of the OpenJML tutorial.

Copyright: You may use and revise these examples for non-commercial purposes as long as you reasonably credit the source, under this Creative Commons License. Fair use (as the term is used in copyright law) for research, publication and education is included in that license.