Features | OpenJML

Currently Supported Features

Tools

Tool	Description	Status
Eclipse/VisualStudio/IntelliJ/LSP integration	Obsolete and not supported; awaiting the creation of an LSP interface for OpenJML	Planned
parsing and type checking	Basic parsing and type attribution of Java and JML	Complete
AST generation, JSON input/output	ASTs can be exchanged in JSON format	Complete
programmatic tool execution	OpenJML can be called programmatically	OK*
static checking tool	See the feature status in the tables linked to the headings on the right	Complete
runtime assertion checking tool	See the feature status in the tables linked to the headings on the right	Complete
jmldoc tool	Tool needs to be reimplemented for Java21	Planned
Test suite generation	JMLUnitNG must be ported to Java21	Not yet supported
high-coverage test case generation	Generating test cases using symbolic execution, guided by specifications; idealy working with respect to a given test suite, so that test additions are found, not just a replacement test suite	Planned
specification discovery	Inferring or guessing specifications from the source code, both loop and procedure specifications	Planned
JML template generation	Generating simple default specifications, to guide the user on what specs need to be written	Planned
multi-threaded checking	Writing and checking specifications for multi-threaded programs.	Planned
specification checking using method inlining	In-lining (non-recursive) methods to avoid needing specifications for all methods.	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: Implemented
- try with resources: Implemented except recording of suppressed exceptions
- Catching multiple exception types
- Type inference: NOT implemented
- Runtime errors associated with varargs parameter lists: NOT implemented
Java 8:
- 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
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
\key	Z	OK	OK	OK	OK	\key 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_captured	2	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
\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_math	2	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 \key 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

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

Level: The level column gives the language level of the feature as defined in the JML Reference Manual.

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)

Sunbelt Computer Software

PL/B Language Development and Support