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.

JML FeatureKeY 1.6.5KeY 2.4.1KeY 2.6Comments
ghost field/variableyesyesyes
model fieldnoyesyes
model methodnoyesyes
class invariantyesyesyessee note below
history constraintnonono
initially clausenoyesyes
axiom clausenoyesyes
represents clausenoyesyes
requires clauseyesyesyes
ensures clauseyesyesyes
signals clauseyesyesyes
signals_only clauseyesyesyes
diverges clauseyesyesyes
measured_by clausenoyesyes
assignable clauseyesyesyes
accessible clausenoyesyes
redundancyyesyesyestreated as non-redundant
set statementyesyesyesknown issue: must not be last statement in block
assert statementnoyesyesknown issue: must be followed by non-empty block
assume statementnonono
visibility modifiersyesyesyes
helper modifiernoyesyes
pure modifiersee noteyesyessee note below
math modifiersnonono
\bigint typenoyes*yesKeY 2.4 uses Euclidean division, mod
\real typenoparsableparsableno reasoning about reals
\TYPE typenonono
\index and \valuesnoyesyesJML extension also used in OpenJML
\invariant_fornoyesyes
\oldyespartiallyyesknown issue: not available for parameters in 2.4
\forall and \existsyesyesyes
\sum\num_of and \productnoyesyes
\min and \maxnonoyes
\freshyesyesyes
\reachnopartiallypartiallyTODO
\typeofyesyesyes
\is_initializedyesyesyes
expression associativityrightrightstandardsee 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 helpermodifier. 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.