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 Feature |
KeY 1.6.5 |
KeY 2.4.1 |
KeY 2.6 |
KeY 2.10 |
KeY 2.12 |
Comments |
| ghost field/variable |
yes |
yes |
yes |
yes |
yes |
|
| model field |
no |
yes |
yes |
yes |
yes |
|
| model method |
no |
yes |
yes |
yes |
yes |
|
| class invariant |
yes |
yes |
yes |
yes |
yes |
see note below |
| history constraint |
no |
no |
no |
no |
no |
|
| initially clause |
no |
yes |
yes |
yes |
yes |
|
| axiom clause |
no |
yes |
yes |
yes |
yes |
|
| represents clause |
no |
yes |
yes |
yes |
yes |
|
| requires clause |
yes |
yes |
yes |
yes |
yes |
|
| ensures clause |
yes |
yes |
yes |
yes |
yes |
|
| signals clause |
yes |
yes |
yes |
yes |
yes |
|
| signals_only clause |
yes |
yes |
yes |
yes |
yes |
|
| diverges clause |
yes |
yes |
yes |
yes |
yes |
|
| measured_by clause |
no |
yes |
yes |
yes |
yes |
|
| assignable clause |
yes |
yes |
yes |
yes |
yes |
|
| accessible clause |
no |
yes |
yes |
yes |
yes |
|
| redundancy |
yes |
yes |
yes |
yes |
yes |
treated as non-redundant |
| set statement |
yes¹ |
yes¹ |
yes¹ |
yes |
yes |
¹known issue: must not be last statement in block |
| assert statement |
no |
yes² |
yes² |
yes |
yes |
²known issue: must be followed by non-empty block |
| assume statement |
no |
no |
no |
yes |
yes |
|
| visibility modifiers |
yes |
yes |
yes |
yes |
yes |
|
| helper modifier |
no |
yes |
yes |
yes |
yes |
|
| pure modifier |
see note |
yes |
yes |
yes |
yes |
see note below |
| math modifiers |
no |
no |
no |
no |
yes |
used integer semantics can be set globally via Taclet options |
| \bigint type |
no |
yes³ |
yes |
yes |
yes |
³KeY 2.4 uses Euclidean division, mod |
| \real type |
no |
parsable |
parsable |
parsable |
parsable |
no reasoning about reals |
| \TYPE type |
no |
no |
no |
no |
no |
|
| \index and \values |
no |
yes |
yes |
yes |
yes |
JML extension also used in OpenJML |
| \invariant_for |
no |
yes |
yes |
yes |
yes |
|
| \old |
yes |
partially |
yes |
yes |
yes |
known issue: not available for parameters in 2.4 |
| \forall and \exists |
yes |
yes |
yes |
yes |
yes |
|
| \sum, \num_of and \product |
no |
yes |
yes |
yes |
yes |
reasoning only about bounded sums and products, e.g. (\sum int i; a<=i<b; f(i)) |
| \min and \max |
no |
no |
parsable |
parsable |
parsable |
|
| \fresh |
yes |
yes |
yes |
yes |
yes |
|
| \reach |
no |
partially |
partially |
partially |
partially |
TODO |
| \typeof |
yes |
yes |
yes |
yes |
yes |
|
| \is_initialized |
yes |
yes |
yes |
yes |
yes |
|
| expression associativity |
right |
right |
standard |
standard |
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
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.