openjml playground

Please take a look at Example.java for some examples on how to use openjml and how to proof.

just openjml

# Only run for specific files
./gradlew clean openjml -Popenjml.mode=esc -Popenjml.files=me/micartey/openjml/Calculator.java

./gradlew clean openjml -Popenjml.mode=esc

Keywords

• loop_invariant: Condition that must be true before the loop begins, at the end of each iteration and upon termination.
• invariant: Class global conditions that need to be correct for an object after creation, modifications (e.g. through setters), etc.
• requires: Pre-Condition for values passed to a method
• ensures: Post-Condition
• assignable: Mark that a field will be modified inside the method
• pure: Method has strictly no side effects. A pure method is guaranteed not to alter the state of any object or variable.
• also: Chain multiple contracts together (e.g. for overwritten methods)
• skipesc: Disable the Extended Static Checking (ESC) and will trust that the method works as intended

Why?

Because testing sucks and this is much better than any test would possibly be. But OpenJML has a long way to go and is not near production ready yet.