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|
|class invariant||yes||yes||yes||see note below|
|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|
|pure modifier||see note||yes||yes||see note below|
|\bigint type||no||yes*||yes||KeY 2.4 uses Euclidean division, mod|
|\real type||no||parsable||parsable||no reasoning about reals|
|\index and \values||no||yes||yes||JML extension also used in OpenJML|
|\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|
|expression associativity||right||right||standard||see note below|
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.
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).
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.