KeY 3.0 released!

[wadoon]

Dear friends of KeY,

I have the pleasure of announcing:

KeY 3.0 is released!

You can find the release here:

https://github.com/KeYProject/key/releases/latest

or on Maven Central under group-id org.key-project

This release is a significant milestone for KeY and would not have been possible without the help of our student assistants over the last two years, the long-term engagement of KeY's friends and users, and the will of the core developers to keep all the ends together. A special thanks to Wolfram for carrying the release with all of its weight over the finish line.

Apropos, the weight of this release:

6500+ changed files, 
 300+ kLoC were added, and 
 435+ kLoC were deleted. 

For comparison, KeY 3.0 consists now of 3760 Java files with 521 kLoC.

A condensed release note with more details is in our docs:

https://keyproject.github.io/key-docs/changelog/

Briefly, I want to highlight some of the new features which emphasize KeY's future:

• KeY is Java25 ready. The parsing architecture got completely replaced. Some new Java constructs are already supported, e.g., Records. Others need deeper investigations on the JavaDL and JML level, which are now enabled.

• With the introduction of parametric sorts, the work on the JavaDL level already began, paving the pathway for the upcoming support of Generics. Sort dependening functions were removed!

• Proof Scripts got promoted to the JML level. You can now help the prover by giving commands with //@ assert ... \by { <script> }; in JML. A step further to reduce the brittleness of proofs.

• We put effort into improving the modularity and extensibility of KeY, making it easier to reuse KeY for your own logic and calculus. This allows, e.g., the once deeply integrated Information-Flow, and Well-definedness calculus to be externalized. These calculi are still usable within the KeY UI. In particular, it enabled the development of native KeY versions for RustyKeY and KeYTher.

Of course, sacrifices were necessary. We could preserve all of KeY's behaviors and functionalities. It is very likely, that this release breaks your old proofs. but help exists in our documentation, or feel free to get in touch with us.

Also, please do not hesitate to report on bugs and issues using Github.

We are looking forward to celebrate with you
on the KeY Symposium in Berlin!

Have a lot fun using KeY!
Alexander