Java 25 Features for KeY

[wadoon]

Please describe your proposal in a ONE sentence

After #3120, we should enable support for Java 25 language features in KeY.

Roadmap

• Generics
• For/in loop
• Autoboxing/Unboxing (Taclets required)
• Typesafe Enums
• Varargs
• Static Import
• (Type) Annotations
  • Reflection is currently omitted in KeY
  • Annotation support for JML?
    • There are JML annotations created by @davidcok for modifiers, e.g., @Pure, etc.
• Binary Literals
• Underscores in Numeric Literals
  • down-compiliation in JP2KEY or covering in KeY-Java-AST
• Strings in switch Statements
  • The byte-code version is complicated of this feature. Translation to if-else-cascade?
• The try-with-resources Statement
  • Down-compilation: try(var x = e) {} ~~> {var x; try{x = e; ...} catch(Exception e) { try{x.close();}catch(Exception e){} }
  • In Java, or Taclet?
• Catching Multiple Exception Types and Rethrowing Exceptions with Improved Type Checking
• Lambda Expressions, ongoing Lambda support by transformation #3759
  • port of @csicar work, down-compilation inner-classes
• Method references
• Default methods
• Repeating Annotations
• Method parameter reflection
  • reflection is not in KeY's scope
• Switch Expressions
  • Requires extension of KeY-Java-AST including yield statement. Another possibility is a down-compilation to switch statement.
• Text Blocks, ongoing Support for TextBlockLiterals #3796 by down-compilation
• Records, ongoing Record support by transformation #3758 by down-compilation
• Sealed Classes
  • Adaption of KeYs resolution mechanism. Activate close-program flag for these classes
• Pattern Matching (switch)
• Pattern Matching (instanceof)
• Record Patterns

Alternatives

A clear and concise description of any alternative solutions or features you've considered.
Why is the suggestion the best alternative?

Estimated effort

If you can: Estimate the effort that has to be invested to implement the feature request.
Is there still discussion needed? Or is it purely implementation? Expertises needed?

Additional context

Add any other context or screenshots about the feature request here.