Java 21 Roadmap

Roadmap for Java 21

Phase One: JavaParser

We have an own fork of JavaParser with support for the KeY-Java extensions.

Deliverable: KeY works the same with Recoder. No direct new support for Java 1.5+.

Phase Two: AST and logics adaptions

New syntactical AST elements are required to capture the features of Java 1.5 to 21. We need to decide which of the new features are represented by AST elements, and which are resolved by translation.

Feature	Solution	Notes
Generics		Diploma of @mattulbrich
For/in loop	AST node + Taclet	Support exists. Coverage unclear
Autoboxing/Unboxing	Taclets required
Typesafe Enums		Attempts exists with down-compiling, but no breakthroughs. (Theory see Mattias' thesis)
Varargs
Static Import
Annotations		Reflection is currently omitted in KeY
Binary Literals		Depending on AST faithfulness
Underscores in Numeric Literals	Depending on AST faithfulness
Strings in switch Statements		The byte-code version is complicated of this feature. Translation to if-else-cascade?
The try-with-resources Statement		Taclets or down-compilation possible.
Catching Multiple Exception Types and Rethrowing Exceptions with Improved Type Checking		seems to be a use-case for taclets
Lambda Expressions		work of Carsten exits, down-compilation inner-classes
Method references
Default methods		no work should be required
Repeating Annotations
Type Annotations		There are JML annotations created by @davidcok for modifiers, e.g., @Pure, etc.
Method parameter reflection		reflection is not in KeY's scope
Switch Expressions	AST node required	down-compilation is not possible easily
Text Blocks	AST node	only for pretty printing. Behaves nearly as String literal
Records		down-compilation possible, Theory for final fields important
Pattern Matching (instanceof)	AST node and taclets
Sealed Classes		Adaption of KeYs resolution mechanism. Activate close-program flag for these classes
Pattern Matching (switch)		down-compilation?
Record Patterns