Syntax Elements

This page is the single reference for the syntax JMLtk understands — plain Java plus the Java Modeling Language (JML) plus KeY’s ProofJava and SchemaJava extensions — element by element, with an example for each. The classes of the AST that represent these elements, and the philosophy behind their naming and structure, are described on the AST Classes page.

Dialect. JML is not standardized: the JML reference manual defines the common core, but the tools interpret it differently. JMLtk tries to follow the reference manual in the common parts, while staying compatible with OpenJML and KeY, and it often accepts a liberal superset of the reference syntax so that all dialects can be parsed. Note that the parser provides no semantics — it lifts the textual JML into an AST, and you, the library user, are responsible for giving the constructs meaning.

Java

JMLtk parses the Java language itself, currently declared to support Java 25 (see the project README.md). The language features tracked since the java-features documentation are the JDK 8 to JDK 17 set below plus the subsequent releases; non-language changes (JVM, GC, packaging — “NA”) are irrelevant for a parser. Language-related changes normally come with a validator used in conjunction with the grammar as part of the parsing process.

JML specification comments

JML lives inside Java comments. JMLtk recognizes two comment shapes:

//@ requires x != null;         // single-line form
/*@ ensures \result >= x; @*/   // block form

They are only processed when JML processing is enabled in the ParserConfiguration (for example setProcessJml(true)); the CLI and the library default the KeY key set on.

Method contracts

A contract groups clauses under a behavioral keyword and is attached to a method, constructor, or block. Behaviors may be joined with also:

/*@ normal_behavior
  @ requires x != null;
  @ ensures \result == x.length;
  @ also
  @ exceptional_behavior
  @ signals (NullPointerException) x == null;
  @*/
public int size(String x) { ... }

Behavioral keywords: behavior, normal_behavior, exceptional_behavior, model_behavior, abrupt_behavior, break_behavior, continue_behavior, feasible_behavior, diverges. Contract elements are clauses; the parser knows the following kinds (JmlClauseKind):

Pre- and postconditions

The _free variants must hold independent of any other contract (they may not be weakened); _redundantly variants may state what follows from the other clauses, helping verification tools.

Frame (assignable) clauses

Location sets are ordinary JML expressions — fields, array ranges (arr[*], arr[i..j]) — including the special sets \nothing, \strictly_nothing and \not_specified.

Exceptional behavior

The signals clause binds the exception variable: signals (E e) P means “whenever e of type E is thrown, P holds”.

Concurrency, resources, termination

Loop specifications (KeY-style keywords)

Block and loop contracts can be written with their own behavior section:

/*@ loop_contract normal_behavior
  @ requires true;
  @ ensures true;
  @ assignable \strictly_nothing;
  @*/
while (cond) { ... }

Class-level members (JmlBodyClauseKind)

Class-level specification elements are clauses of the body package:

Model, ghost and spec state

• model fields and methods are specification-only members with no Java implementation; ghost declarations introduce specification variables that can be assigned by JML statements (see statements); both carry the model/ghost modifiers (below).
• represents connects a model field to concrete state (JmlRepresentsDeclaration):

//@ model int size;
//@ represents size <- items.length;

//@ ghost int count;
//@ model public static boolean conversionBad(String s);

• spec_public, spec_package, spec_protected, spec_private widen the Java visibility for specification access.

JML expressions

Quantified expressions

The reference quantifiers — \forall, \exists, \max, \min, \sum, \product, \num_of — are supported, followed by a bound-var declaration with an optional bound-var modifier, a ;, one or more predicates, and the body:

//@ ensures (\forall int i; 0 <= i && i < a.length; a[i] > 0);
//@ ensures (\sum int i; 0 <= i && i < n; a[i]) == total;
//@ ensures (\num_of int i; 0 <= i && i < n; a[i] == 0) == zeros;

The grammar is deliberately more liberal than the reference so that all dialects parse: a quantified expression is

"(" quantifier bound-var-decls ";" Expression (";" Expression)* ")"

i.e. as many range expressions as you like. This also covers the KeY form of a bounded sum with lower and upper bound:

//@ ensures (\bsum int i; i > 0; i <= n / 2; 2 * i) == total;

Since the reference manual only knows seven quantifiers with at most two bound expressions, you are responsible for raising an error if your tool cannot handle an unusual combination. Represented by JmlQuantifiedExpr.

\let, \old and friends

The full inventory of specification keywords the lexer recognizes includes \all_fields, \all_objects, \empty, \emptyset, \seq_singleton, \seq_concat, \seq_get, \seq_length, \seq_put, \seq_reverse, \seq_sub, \set_union, \set_minus, \intersect, \infinite_union, \subset, \singleton, \locset, \lockset, \nonnullelements, \not_assigned, \not_modified, \only_assigned, \only_accessed, \only_called, \only_captured, \same, \new_elems_fresh, \new_objects, \static_invariant_for, \invariant_for, \is_initialized, \java_math, \bigint_math, \safe_math, \from_goal, and the \lbl-marked formulas used by KeY proof scripting.

Relational chains

JML allows chaining comparison operators as a conjunction; JMLtk parses them into a single multi-comparison node (JmlMultiCompareExpr):

//@ requires 0 <= x <= a.length;      // 0 <= x && x <= a.length
//@ ensures  i < j <= n;

Infix set and subtype operators

The lexical level permits infix use of the set operators (JmlBinaryInfixExpr keeps the operator token as a name): a \cup b \cap c, \subset, \intersect, \set_union, \set_minus, … and the subtype operator <::

//@ ensures \typeof(\result) <: \type(Exception);
//@ ensures s1 \subset s2 \cup s3;

Set comprehensions

//@ ensures seen == { int i; 0 <= i && i < n; a[i] };   // JmlSetComprehensionExpr

Logic types

Specification-only types are parsed into JmlLogicType:

\bigint    mathematical arbitrary-precision integer
\bigfloat  mathematical real (bit-exact floats)
\real      mathematical reals
\locset    location set (a "store" of assignable locations)
\seq       immutable sequences of values
\set       finite sets of values
\map       total or partial maps (KeY)

JML statements

Inside method bodies, JML contributes statements (ast/jml/stmt):

In addition, spec-only expressions can appear as statements via JmlExpressionStmt.

Merge points

A state-merging (abstraction) point tells the verification tool where and how to merge symbolic execution states, as used by KeY’s state-merging:

//@ merge_point \by "MergeByPredicateAbstraction"
//@     \lattice conjunctive
//@     \predicate (int x) : x >= 0, x == \old(b) || x == -\old(b);

All three options are optional and must appear in this fixed order: \by, then \lattice, then \predicate. The values of \by and \lattice may be given as a string literal or as a plain identifier; both forms are normalised to a StringLiteralExpr in the AST. \predicate binds a variable of the given type and lists the abstraction predicates separated by commas. AST node: JmlMergePointStmt (properties by, lattice, predicateVariable, predicates).

merge_point is a contextual keyword, not a reserved word: it is recognized as a merge point only when directly followed by ; or one of the \by / \lattice / \predicate options, in method bodies as well as in JML comments. The KeY spelling $mergePoint is accepted too. When followed by (, as in the old KeY ProofJava form merge_point ( expr );, it is an ordinary method invocation (MethodCallExpr), not a merge point — and merge_point can be used as a plain identifier (fields, local variables, method names).

Modifiers

JML modifiers appear together with Java modifiers on members and fields (Modifier class, JML_* keywords). The parser knows:

ghost   model   helper   instance
nullable   non_null   non_null_by_default   nullable_by_default
nonnullelements
spec_public   spec_package   spec_protected   spec_private
no_state   two_state
code   code_java_math   code_bigint_math   code_safe_math
spec_java_math   spec_bigint_math   spec_safe_math
peer   rep   read_only

For example:

public class Bag {
    private /*@ spec_public @*/ int n;
    private /*@ non_null @*/ int[] items;
    //@ ghost int count;
    //@ model int capacity;
    //@ invariant 0 <= n && n <= items.length;
    //@ invariant n == count;
}

KeY extensions — ProofJava

KeY’s theorem prover needs constructs that do not occur in ordinary Java. ProofJava (PJava) adds information used during a proof in KeY’s sequent calculus on JavaDL; SchemaJava (SJava) adds placeholders for tree matching. Both are parsed by JMLtk into the ast/key packages. The constructs below are the differences on top of JML-Java.

Method frames

A method frame stores the context of a Java block that may be lost by method inlining; the execution context fixes the source declaration and, optionally, the this instance:

method-frame ( [ result-> <name>, ]
               source = <method-signature>@<type>
               [, this = <expr>] )
    <block>

AST nodes: KeyMethodCallStmt with a KeyExecutionContext, KeyMethodSignature.

Method calls with a target type

The result type of an expression is written explicitly:

<expr> @ <type>;
<name> = <expr> @ <type>;

AST node: KeyMethodBodyStatement.

Java Card transaction markers

#beginJavaCardTransaction ;
#commitJavaCardTransaction ;
#finishJavaCardTransaction ;
#abortJavaCardTransaction ;

AST node: KeyTransactionStmt.

Merge points

The KeY ProofJava form merge_point ( <expr> ); is no longer a dedicated statement: the KeyMergePointStmt AST node was removed. Because merge_point is a contextual keyword, the form still parses — as an ordinary method invocation (ExpressionStmt wrapping a MethodCallExpr), so existing ProofJava sources keep parsing. The JML merge-point statement with the \by/\lattice/\predicate options is JmlMergePointStmt — see JML statements.

Loop scopes

loop-scope ( <expr> ) <block>

AST node: KeyLoopScopeBlockStmt.

Catch-all statements

A #catchAll statement targets the exception variable and wraps a block:

#catchAll ( <name> ) <block>

AST node: KeyCatchAllStmt.

exec with catch-clauses

exec <block>
[ ccatch ( \Return ) <block> ]
( ccatch ( \Return <type> <id> ) <block> )*
[ ccatch ( \Break ) <block> ]
( ccatch ( \Break <id> ) <block> )*
[ ccatch ( \Break * ) <block> ]
[ ccatch ( \Continue ) <block> ]
( ccatch ( \Continue <id> ) <block> )*
[ ccatch ( \Continue * ) <block> ]
( ccatch ( <parameter> ) <block> )*

AST nodes: KeyExecStmt with KeyCcatchBranch, KeyCcatchReturn, KeyCcatchBreak, KeyCcatchContinue, KeyCcatchParameter.

Passive expressions

@( <expr> )

A passive expression has no side effects. AST node: KeyPassiveExpression.

Implicit identifiers

KeY uses a third kind of identifier — Java identifiers enclosed in angle brackets:

<result>
<count>

AST node: KeyEscapeExpression and the implicit-id handling in the lexer.

No-body constructors and methods

KeY allows declarations without a body (the grammar covers bodies as optional):

class String { public String(); }

KeY extensions — SchemaJava

SchemaJava adds schema variables (SVs) — placeholders that allow writing AST patterns — plus meta-constructs for term rewriting.

Schema variables

A schema variable is a regular identifier starting with # (not allowed to start with a digit):

#a + #b
(#T) (#b - #q)
class #NAME { }
#var + 2 - obj.abc()
#obj.#field1.#field2.#method(#arg1, #arg2);

A schema variable may occur anywhere a normal identifier can, and its meaning is refined by position (as a type, as a statement, …). The typed schema variables are KeyVariableSV, KeyTypeSV, KeyStatementSV, KeyExpressionSV, KeyMethodSignatureSV, KeyProgramVariableSV, KeyCatchClauseSV, KeyCcatchSV, KeyJumpLabelSV, KeyExecCtxtSV.

Contextual blocks

A block annotated with context (start/end markers { . ... .. ... ... } and { .. ... ... }):

{ . <method-signature>@<type>(<expr>)  .. <statements>  ... }
{ . <exec>  .. <statements>  ... }
{ .. <statements>  ... }
{ <statements> }

AST node: KeyContextStatementBlock.

Static evaluation

#evaluate( <expr> )

Schema types

<schemaId>
#typeof( <expr> )

AST node: KeyTypeSV, KeyMetaConstructType.

Meta-construct statements

A series of statement-level meta constructs for rewriting:

#unwind-loop ( <label>, <label>, <loopStatement> );
#unwind-loop-bounded ( <label>, <label>, <loopStatement> );
#FORINITUNFOLDTRANSFORMER( ForInit );
#LOOPSCOPEINVARIANTTRANSFORMER( <whileStatement> );
#unpack ( <forStatement> );
#for-to-while ( <label>, <label>, <statement> );
#switchof ( <statement> );
#do-break ( <labeledStatement> );
#evaluate-arguments ( <expression> );
#replace ( <statement>, <variable> );
#method-call ( [<variable>,] [<variable>,], <primaryExpression> );
#expand-method-body ( <statement> [, <variable>] );
#constructor-call ( <variable>, <variable> );
#special-constructor-call ( <variable> );
"#post-work" ( consRef = ExpressionSV() ) ";"
"#static-initialisation" ( activeAccess = PrimaryExpression() ) ";"
"#resolve-multiple-var-decl" ( stat = Statement() ) ";"
"#array-post-declaration" ( stat = Statement() ) ";"
"#init-array-creation" ( sv = VariableSV(), consRef = ExpressionSV() ) ";"
"#init-array-creation-transient" ( sv = VariableSV(), consRef = ExpressionSV() ) ";"
"#init-array-assignments" ( sv = VariableSV(), consRef = ExpressionSV() ) ";"
"#enhancedfor-elim" ( loopStat = ForStatement() ) ";"
<REATTACHLOOPINVARIANT> ( loopStat = WhileStatement() ) ";"

AST node: KeyMetaConstruct and KeyMetaConstructExpression.

Compatibility notes (deviations)

JMLtk may parse more than it can interpret. The following notes from the original documentation describe the known edges:

KeY

• the parser supports the JML merge_point statement at the syntactic level (see above); the KeY ProofJava form merge_point ( expr ); is parsed as an ordinary method invocation; no dedicated support for information-flow contracts;
• unclear whether x instanceof int should be accepted;
• KeY puts no modifiers in contracts and allows modifiers in arbitrary positions; JMLtk follows JML in requiring modifiers before the return type.

OpenJML

• non_null_by_default is accepted as a modifier (see modifiers), but openJML-style static public datatype N {} declarations are not;
• multi-line contracts written with single-line comments are handled leniently;
• contract modifiers should not be part of the contract:

  //@ model public static void conversionBad(nullable String s, Object o) {
  //@   ghost string s4 = o; // error
  //@ }
• //@ reachable; and the static_initializer / readonly modifiers are not supported.

Extensions beyond the JML reference

• infix set operators: a \cup b \cap c (see above);
• relational chains: 0 <= x <= a.length (see above);
• block / loop contracts with behavior sections (KeY, see above);
• heap on clauses: heap quantifiers written on the clause:

  requires<trans><h> true;
  ensures<h1><h2> true;
• the determines / separates family (extended clause kinds).

Differences from upstream JavaParser

For maintainers, the structural changes vs. the upstream JavaParser grammar (JMLtk is a fork):

• No-body constructors are allowed (KeY);
• New statement node types — KeyMetaConstruct, KeyMethodCallStatement, KeyMethodBodyStatement, KeyTransactionStatement, KeyLoopScopeBlock, KeyCatchAllStatement, KeyExecStatement and their KeyCcatch* parts;
• New primitive logic types — \bigint, \real, \locset, \seq, \free, \map;
• New types — schema types and meta-types (see SchemaJava);
• New modifiers — ghost, model, no_state, two_state;
• A lot of new tokens (all the JML keywords above), each declared with its own lexer rule and classified in TokenTypes#getCategory.

See the AST Classes page for how all of this is reflected in the node hierarchy, and the Development section for the grammar itself (javaparser-core/src/main/javacc/java.jj).