JML Support in KeY

This page documents the state of support for the Java Modeling Language (JML) in KeY releases 1.6.5 and 2.4.1 as well in the release candidate for KeY 2.6.0. We also list some KeY-specific extensions to JML here. We do not explain JML itself here, please refer to the reference manual for that.

	KeY 1.6.5	KeY 2.4.1	KeY 2.6 RC	Comments
ghost field/variable	yes	yes	yes
model field	no	yes	yes
model method	no	yes	yes
class invariant	yes	yes	yes	see note below
history constraint	no	no	no
initially clause	no	yes	yes
axiom clause	no	yes	yes
represents clause	no	yes	yes
requires clause	yes	yes	yes
ensures clause	yes	yes	yes
signals clause	yes	yes	yes
signals_only clause	yes	yes	yes
diverges clause	yes	yes	yes
measured_by clause	no	yes	yes
assignable clause	yes	yes	yes
accessible clause	no	yes	yes
redundancy	yes	yes	yes	treated as non-redundant
set statement	yes	yes	yes	known issue: must not be last statement in block
assert statement	no	yes	yes	known issue: must be followed by non-empty block
assume statement	no	no	no
visibility modifiers	yes	yes	yes
helper modifier	no	yes	yes
pure modifier	see note	yes	yes	see note below
math modifiers	no	no	no
\bigint type	no	yes*	yes	KeY 2.4 uses Euclidean division, mod
\real type	no	parsable	parsable	no reasoning about reals
\TYPE type	no	no	no
\index and \values	no	yes	yes	JML extension also used in OpenJML
\invariant_for	no	yes	yes
\old	yes	partially	yes	known issue: not available for parameters in 2.4
\forall and \exists	yes	yes	yes
\sum, \num_of and \product	no	yes	yes
\min and \max	no	no	yes
\fresh	yes	yes	yes
\reach	no	partially	partially	TODO
\typeof	yes	yes	yes
\is_initialized	yes	yes	yes
expression associativity	right	right	standard	see note below

Notes

Class Invariants

KeY does not require invariants to hold in every visible state. In KeY 1.6.5 or older, invariants are required to hold in the post state. The user has to select in the GUI which invariants are assumed for each method. In KeY 2.0.0 or later, invariants are not generally assumed in pre conditions or required in post conditions. The only exception are invariants of the class (or a superclass) in which the method under test is declared. This behavior can be disabled using the helper modifier. Invariants can be explicitly added to any specification clause using the \invariant_for expression.

Purity

In KeY 1.6.5 or older, the pure modifier means strong purity (no changes to the heap at all). In KeY 2.0.0 or later, it means weak purity as described in the JML reference manual. For strong purity use the strictly_pure modifier instead (KeY-specific extension).

Expression Associativity

The JML reference manual declares all operators to be left-associative (as in Java), with the exception of the forward implication, which is right-associative. Only KeY versions from 2.6.0 on respect this. In earlier versions, all operators are right-associative. When using those, remember that KeY is not a replacement for a JML syntax/type checker.