THIS PAGE IS OUT OF DATE

Currently Supported Features

Tools

Tool Description Status
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 Complete
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 Specifications shown for all Java elements; needs implementation of model methods and model classes Planned
Test suite generation See JMLUnitNG Complete
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 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
\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 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_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: Level: The level column gives the language level of the feature as defined in the JML Reference Manual.