OpenJML Features
These tables list the various features of JML and their status within OpenJML.
Tools
Java language elements
General JML features
Types specifications
Method specifications
Field specifications
JML types
JML expressions
Store-ref expressions
JML Statements
Modifiers
OpenJML extensions to JML
Deprecated syntax
Key:
- OK = implemented within OpenJML
- OK* = implemented with some restrictions
- -- = implemented with significant restrictions
- X = not or only partially implemented
- ? = definition of the feature is under discussion
- 0 = supported by a minimal tool
- 1 = supported and used by most tools and specifications
- 2 = generally useful but more specialized features
- 3 = uncommonly used features
- C = features related to concurrency
- X = experimental features
- Z = extensions (not defined as even experimental for JML)
Tools
| Eclipse integration | Problem indication, source code browsing, auto static checking and runtime compilation, counterexample browsing are implemented; syntax coloring, JML_aware editing is in planning |
| static checking tool | See the feature status in the tables below |
| runtime assertion checking tool | See the feature status in the tables below |
| jmldoc tool | Planned - specifications shown for all Java elements; needs implementation of model methods and model classes |
| Test suite generation | See JMLUnitNG |
| high-coverage test case generation | Planned |
| specification discovery | Planned |
| .jml template generation | Planned |
| multi-threaded checking | Planned |
| specification checking using method inlining | Planned |
Java language elements
Except where indicated, all Java language elements through Java 7 are parsed, typechecked and compiled in RAC. Some elements are not modeled by OpenJML logic or have the corresponding checks inserted in RAC- Java through Java 4: All features are modeled and checked except
- Enum classes
- The synchronized modifier
- The strictfp modifier
- The volatile, transient, native modifiers
- Java 5:
- Generic types : partially modeled by ESC.
- Enhanced for loop: Modeled and checked using JML's loop annotations
- Autoboxing/unboxing: (OK for Java, needed yet for JML expression)
- Typesafe enums : enums are not modeled by ESC; they are compiled but not checked by RAC
- Static import : OK ( but JML model imports are treated just like Java imports)
- Varargs : Not yet modeled or checked
- Java annotations : No checks on annotations are modeled by ESC or compiled by RAC.
- Java 6: No language changes
- Java 7:
- binary literals: Implemented
- literals with underscores: Implemented
- Strings in switch statements: Compiled in RAC, but NOT modeled or checked
- try with resources: Compiled in RAC, but NOT modeled or checked
- Catching multiple exception types: NOT modeled or checked
- Type inference: NOT implemented
- Runtime errors associated with varargs parameter lists: NOT implemented
- Java 8: (OpenJML is only implemented at present for Java through Java 7)
- lambda expressions
- enhancements to annotations (including JSR308)
General JML features for ESC and RAC
Level Parser Type Checker Static Checker Runtime Checker Comments JML annotation comments 0 OK OK OK OK Optional JML annotations (e.g. //+ESC@ ) 0 OK OK OK OK model imports 1 OK OK* OK* OK* Model imports are treated just like regular Java imports nowarn annotations 2 OK OK OK OK JML modifiers as Java annotations (e.g. @NonNull) 0 OK OK OK OK Specification files (.jml) 0 OK OK OK OK The search algorithm for specification files is not standardized Specifications in class files (via JIR or BML) X X X X Not yet implemented. Library specifications 0? OK* OK OK OK Many JDK library specifications must still be written and tuned to static and runtime checking. RAC compiles checks into the caller, but not into the library itself. field, method, constructor keywords 2 OK X X X These keywords are simply parsed and ignored \not_specified 0 OK OK OK OK OpenJML treats a specification clause using \not_specified the same as if the clause were not present. Synonyms 0 OK OK OK OK All JML keyword synonyms are implemented (e.g. exsures, pre, post, assignable vs. modifiable, behaviour vs. behavior) *_redundantly keywords 1 OK OK -- -- Keywords ending in _redundantly are treated just like the corresponding non-redundant keyword; ideally they are handled differently by ESC or can be separately disabled in RAC Java or JML comments embedded in JML comments Z? OK OK OK OK It is under discussion whether embedded comments are legal syntax. Type specifications
Level Parser Type Checker Static Checker Runtime Checker Comments ghost fields 0 OK OK OK OK model fields 0 OK OK OK* OK* Model fields have tricky semantics in ESC; RAC implements model fields incompletely for inherited fields and represents clauses model methods 1 OK OK OK OK model classes and interfaces 3 OK OK OK OK invariant 0,1 OK OK OK OK instance invariants are Level 0; static invariants are level 1 constraint 1 OK OK OK* OK* The optional 'for' suffix of constraint clauses is not checked represents 0,2 OK OK OK OK* Functional represents clauses are level 0; \such_that clauses are level 2; RAC/ESC need implementation for multiple or inherited represents clauses axiom 1 OK OK OK N/A When checking a method, axioms are included for all classes mentioned in the body of the method. initially 0 OK OK OK OK initializer, static_initializer 1 OK OK OK OK Method specifications
Level Parser Type Checker Static Checker Runtime Checker Comments inherited specifications 0 OK OK OK OK lightweight specifications 0 OK OK OK OK heavyweight specifications 0 OK OK OK OK implies_that specifications 1 OK OK X X parsed, checked, and ignored for_example specifications 1 OK OK X X parsed, checked, and ignored model programs 2 OK OK X X parsed, checked, and ignored code modifier 3 OK OK OK OK requires 0 OK OK OK OK ensures 0 OK OK OK OK signals 0 OK OK OK OK signals_only 0 OK OK OK OK Some outstanding implementation issues with default clauses modifies,assignable,modifiable 0 OK OK OK* OK Checks of assignable statements are implemented, but the appropriate havoc statements on calling a method with array index range expressions are imcomplete diverges 2 OK OK X X forall 1 OK OK X X old 1 OK OK OK OK callable 2 OK X X X accessible 2 OK OK X X captures 2 OK OK X X when C OK OK X X measured_by 2 OK OK X X duration, working_space 2 OK OK X X choose, choose_if 2 OK X X X model program continues, breaks, returns statements 2 OK* X X X Optional labels on these statements is not parsed. Field specifications
Level Parser Type Checker Static Checker Runtime Checker Comments in 0 OK OK OK OK maps 1 OK OK X X readable, writable 2 OK OK X X monitors_for C OK OK X X JML types
Level Parser Type Checker Static Checker Runtime Checker Comments \TYPE 0 OK OK OK* OK* There is some cleanup to be done of the semantics and implementation of \TYPE in conjunction with Java generics \bigint 1 OK OK X X see Chalin, 2004 \real 2 OK OK X X JML expressions
Level Parser Type Checker Static Checker Runtime Checker Comments ==> <== <==> <=!=> operators 0 OK OK OK OK <: operator (subtype) 0 OK OK OK OK <# <=# operators C OK OK X X These are lock-ordering operators pure method calls in specification expressions 1 OK OK OK OK No recursion allowed, currently \result 0 OK OK OK OK \old, \pre 0 OK OK OK OK There are on-going discussions about the semantics of cross-state comparisons \past ? OK OK OK OK This feature is under discussion as an addition or replacement for \old \fresh 0 OK OK OK X \nonnullelements 0 OK OK OK (uses quantification) OK \elemtype 0 OK OK X X \typeof 0 OK OK OK OK \type 0 OK OK OK OK \lblneg, \lblpos 2 OK OK OK OK \lbl Z OK OK OK OK \lbl is an extension Quantified expressions: \forall, \exists, \max, \min 0 OK OK OK* OK* RAC is implemented for expressions with just one declaration; not all provers handle quantification Quantified expressions: \num_of, \sum, \product 1 OK OK X OK* RAC is implemented for expressions with just one declaration; proposed extensions not yet implemented. SMT solvers do not generally handle induction well, as needed for these operators. Set comprehension 1 OK OK X X There are outstanding issues regarding this feature \not_modified 2 OK OK -(not implemented for model fields or for o.*, a[*] and a[..] syntax, semantics for x.f is under consideration) -(same as above) \not_assigned, \only_accessed
\only_assigned, \only_called, \only_captured2 OK X X X \reach 2 OK OK X X \is_initialized 2 OK OK X X \invariant_for 2 OK OK X X \duration, \space, \working_space 3 OK OK X X \lockset, \max C OK X X X \same 3 OK OK X X semantics needs clarification \index, \values Z OK OK OK X Extensions to specify for-each loops \peer, \rep, \readonly 0,X X X X X \warn_op, \warn, \nowarn_op, \nowarn 2 OK OK X X Parsed, but treated as a no-op \java_math, \safe_math, \bigint_math 2 OK OK OK* OK* Partially implemented Informal expression 0 OK OK OK OK The (* *) form is translated to true; the proposed functional form - JML.informal(\_) - is also implemented. Let expression (introduced at Dagstuhl 2009) ? OK OK OK OK Would be nice to have a such-that form of let. Store-ref expressions
Level Parser Type Checker Static Checker Runtime Checker Comments \nothing, \everything 0 OK OK OK OK x, o.f, T.f, a[i] syntax 0 OK OK OK OK o.*, T.*, a[1..2], a[*] syntax 2? OK OK OK OK a[1..] syntax Z OK OK OK OK JML statements
Level Parser Type Checker Static Checker Runtime Checker Comments specifications on local Java class declarations 1 OK OK OK OK The specs are checked to the extent they are on other declarations specifications on anonymous class declarations 1 OK OK OK OK The specs are checked to the extent they are on other declarations ghost variable declarations 0 OK OK OK OK assert statement 0 OK OK OK OK assume statement 0 OK OK OK OK set statement 0 OK OK OK OK Need to clarify the permitted syntax debug statement 2 OK OK OK OK Need to clarify the permitted syntax loop_invariant 0 OK OK OK OK decreases 1 OK OK OK OK refining 2 OK OK X X unreachable 2 OK OK OK OK reachable 2 OK OK OK OK This is an extension hence_by 2 OK OK X X Modifiers on JML declarations
JML modifiers can be expressed in either JML form (e.g. /*@ pure */) or in Java form(e.g. @org.jmlspecs.org.Pure).Level Parser Type Checker Static Checker Runtime Checker Comments public, protected, private 0? OK OK OK OK spec_public, spec_protected 0 OK OK OK OK instance, static on interface declarations 0 OK OK X X is instance allowed anywhere? helper 0 OK OK OK OK ghost, model OK OK OK OK pure 1 OK OK OK OK Pure is implemented but is too strong to be useful; see secret and query monitored C OK OK X X uninitialized 1 OK OK X X query, secret Z OK OK OK* OK* Extension code_bigint_math, code_java_math, code_safe_math,
spec_bigint_math, spec_java_math, spec_safe_math2 OK OK OK* OK* non_null, nullable 0 OK OK OK OK nullable_by_default 0 OK OK OK OK This one or its complement is an extension non_null_by_default 0 OK OK OK OK This one or its complement is an extension Universe types: peer, rep, \peer, \rep 0 OK X X X Universe annotations are parsed and ignored Universe types: readonly, \readonly X OK X X X Universe annotations are parsed and ignored extract 2 OK? X? X? X? Insufficiently defined in the reference manual OpenJML extensions to JML
- The \lbl expression
- The \values and \index expressions (used with for-each loops)
- The \distinct expression
- Flexibility in writing method specifications? Optional 'also'? an else?
- Query and Secret annotations
- The use of Java or JML comments within JML comments
- Predefined ESC and RAC and DOC and DEBUG annotation keys
- Predefined JAVA4 JAVA5 JAVA6 JAVA7 annotation keys
- The reachable statement
Deprecated syntax
- The refine and refines statements; Specifications contained in files with suffixes other than .jml and .java; in addition, the algorithm for finding specification files has changed.
- The mechanism for specifying optional annotations has changed; //+@, /*+@, //-@ and /*-@ are all deprecated in JML. OpenJML ignores //-@ and /*-@ comments and accepts //+@ and /*+@ comments for now because there are such comments in the library specifications, since ESC Java uses them.
- The <- form of the represents clause is deprecated, though it is still supported by OpenJML.
- JML annotations within Javadoc comments are not supported by OpenJML; they are or will soon be deprecated by JML.
Last modified Nov 14 2025.