KeY-3.0.0

What's Changed

Breaking Changes 🗲

• Set the Java Release Version to 21 by @wadoon in #3522
• Removal of Triple, and Quadruple by @wadoon in #3529
• Use KeYParser.g4 for parsing proof scripts by @wadoon in #3021
• Migration to java.nio.Path by @wadoon in #3618
• Refactoring context menus of sequent views by @wadoon in #3641
• AST for KeY Scripts by @wadoon in #3587
• Higher Order Proof Scripts by @wadoon in #3654
• Modularization: InfFlow and WD as separate modules by @wadoon in #3640
• Make the context menu more flexibel and type safe. by @wadoon in #3785
• Purge sort depending functions in favor of parametric functions by @Drodt in #3773
• Make \sameUpdateLevel the default by @Drodt in #3899

Exciting New Features 🎉

• Extract Taclets and Prover Main Loop to ncore by @Drodt in #3578
• Renovation of the TestCase generation by @wadoon in #3388
• Add Polymorphic Sorts and Functions by @Drodt in #3652
• The Removal of Recoder by @wadoon in #3120
• Proof Scripts in JML by @mattulbrich in #3657

Features

• Proposing a more flexible lexing framework by @mattulbrich in #3537
• highlight current line in issue editor pane by @mattulbrich in #3573
• Improved treatment of final fields by @mattulbrich in #3495
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in #3594
• SMT test cases rework by @WolframPfeifer in #3592
• Isabelle Translation by @BookWood7th in #3514
• Introducing some structure for model method bodies by @mattulbrich in #3571
• Linearized symbolic execution in proof tree by @FliegendeWurst in #3237
• KeY/JSON config for SMT solvers by @wadoon in #3597
• Save proof independent settings, that are not used by the configuration by @PiIsRational in #3700
• Send Feedback using Github issues by @wadoon in #3736
• Pfeifer/proof mgmt includes fix by @WolframPfeifer in #3757
• Add sort aliases by @Drodt in #3778
• Give similar taclet names if taclet not found during proof loading by @wadoon in #3784
• Add support for Annotation Processors in the Javac Extension by @PiIsRational in #3686
• Options Panel in Load Dialog. Options in Recent Files by @wadoon in #3788
• Add support for var variable declarations by @Drodt in #3821
• Basic Theory of Sets by @WolframPfeifer in #3777
• Collapsing proof search by @unp1 in #3825
• Improvements for the Taclet Match Dialog by @unp1 in #3830
• Allow realizing multiple cached branches at once by @FliegendeWurst in #3440
• automode to choose from a dropdown list by @mattulbrich in #3857
• Feature: Version-based Configuration Paths by @wadoon in #3888
• Fix compact constructor in Records by @wadoon in #3905
• Soundiness dialog for making assumptions explicit by @mattulbrich in #3887

Bug Fixes

• Add conversion rules for Float/Double negation by @WolframPfeifer in #3520
• Fix #3524 by @Drodt in #3525
• Fixing the broken automode by @mattulbrich in #3533
• Fix #3452 by @wadoon in #3540
• fix #3553 by @MarcoScaletta in #3560
• Fix #3563 by @Drodt in #3566
• Fix line number alignment in SMT interface by @BookWood7th in #3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in #3543
• fixing lexing to support static invariants by @mattulbrich in #3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in #3593
• Fix Java version in nightlydeploy.yml by @wadoon in #3598
• Fix exception in javac extension by @FliegendeWurst in #3609
• fix testMakeFilenameRelativeWindows by @wadoon in #3619
• Disable relative path test on Windows by @wadoon in #3629
• Fix SMT ApplyAction not pruning when undoing by @BookWood7th in #3606
• Fix NPE using KeY command line interface caused by Java NIO by @wadoon in #3643
• FIX: URGENT: Changes in Gradle 9 results into non-execution of custom test tasks. by @wadoon in #3653
• fix css for sequentview syntaxhighlightning by @wadoon in #3645
• Allow true in more JML expressions by @mattulbrich in #3664
• Fix NPE in dependency contract feature (caused by pulled out expression) by @unp1 in #3675
• Fix Information Flow Proof Loading for KeY Jar File by @Drodt in #3678
• Enable assertion for :key.ui:run by @wadoon in #3682
• Fix proof task tree forced white background. by @wadoon in #3663
• Fix deadlock when showing JML warnings dialog by @FliegendeWurst in #3692
• Check for applicability of Antec-/SuccTaclets in Proof Replay by @Drodt in #3702
• Return to Metal as default Look and Feel by @WolframPfeifer in #3658
• fix #3721, getParent().toUri() requires absolute paths by @wadoon in #3722
• Fix unbalanced block exception when pretty printing heap terms by @unp1 in #3726
• Add reachable Java state properties to invariant for modified local variables (fixes #3728) by @unp1 in #3747
• Fix for #3738: Fix SMT type axiomatisation for interfaces by @WolframPfeifer in #3749
• Anonymize ghost variables in loop by @Drodt in #3729
• Proof Management: Ignore internal contracts when calculating dependency state (fixes #3745) by @WolframPfeifer in #3748
• Fix for #3683: Hiding package prefixes in sequent view by @WolframPfeifer in #3684
• Taclet definition added to problemHeader by @wadoon in #3733
• put CachingExtension into the correct service file. by @wadoon in #3782
• move Taclet options of WD from key.core to key.core.wd by @wadoon in #3783
• Allow KeY to start even in case of unreadable recent files by @unp1 in #3790
• ProofManagement extension: Iterative NodeIntermediateWalker to avoid stack overflows by @WolframPfeifer in #3793
• Dependency Contract: Ignore all term labels when searching for base term by @FliegendeWurst in #3776
• Alternative for #3393: Fix slicing bug related to Evaluate Query by @WolframPfeifer in #3794
• Fix field names in Isabelle translation by @unp1 in #3795
• Enable KeY to distinguish between classes of same name in different packages by @unp1 in #3805
• Improve behavior in case of not found methods by @unp1 in #3806
• Fix naming and renaming issues by @unp1 in #3804
• Fix Path bug by @wadoon in #3810
• Fix bug in ProofManagementDialog by @unp1 in #3812
• Fix 'choose contract' in parser by @Drodt in #3840
• Fixes for minor regressions on main by @unp1 in #3844
• Make new name creation only dependent on goal namespaces not on global counter by @unp1 in #3848
• Fix per-proof memory leak: clear JavaParserFacade cache on dispose by @unp1 in #3854
• Make cross-platform path/URI/charset handling in load/save more robust by @unp1 in #3860
• Fix "Rule of same name exists already" error after pruning (rare but occuring cases after mass pruning with try-closeable-goals) by @unp1 in #3850
• Fix most-recent file not set after loading recent-files list (#3711) by @unp1 in #3866
• Reject generic sorts at user-input boundaries: \problem, JML, taclet instantiation (#3409) by @unp1 in #3869
• Fix fast-click auto-mode crash: overlapping runs + proof breaking proof listeners by @unp1 in #3880
• Fix NPE when copying a namespace set with a root sub-namespace by @unp1 in #3881
• Follow-up fixes for cost-reuse: remove unsound static caches by @unp1 in #3873
• Implement \real literals (#3570); fix LogicPrinter.quickPrintSemisequent (#243) by @unp1 in #3865
• Fix changing Taclet Options via the GUI (and more) + TimSort source files added as examples by @unp1 in #3889
• Fix two soundness gaps in select/permission taclets by @unp1 in #3891
• Cost-Reuse: Fix latent classification bugs and code cleanup by @unp1 in #3890
• Fix GUI crashes when no proof is loaded, and remove dead MainWindowTabbedPane by @unp1 in #3892
• Fix for DepthFirstGoalChooser: Keep enabled sibling goals on a split by @unp1 in #3886
• Fix finalFields default in FinalHeapResolution.isFinalEnabled by @unp1 in #3895
• Fixes "No Proof" in status line when a proof was closed. by @unp1 in #3900
• Ensure default option for pruning/disposing of cache sources is set properly by @WolframPfeifer in #3901
• Microfix: Missing ',' in CLUTTER_RULES prevented rules to be lower prioritized (as their two name were joined together) by @unp1 in #3906
• Fix pruning of cached branches by @FliegendeWurst in #3858
• Fix broken proof tree after information flow auto pilot by @unp1 in #3911
• Respect the \profile declaration of loaded files again by @unp1 in #3912
• Use default key stroke settings when no settings file exists by @unp1 in #3913
• Fix: Automode button in Strategy Pane could not be used to stop automode by @unp1 in #3896
• Fix file dependency for runAntlr4KeY by @Drodt in #3920
• Enforce profile when selected via file chooser by @unp1 in #3921
• Only recreate Isabelle session files if path has actually changed by @flo2702 in #3929
• Removed double dbg msg by @flo2702 in #3930

Dependencies

• Bump the gradle-deps group with 5 updates by @dependabot[bot] in #3516
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in #3517
• Bump the gradle-deps group with 6 updates by @dependabot[bot] in #3527
• Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in #3526
• Bump the github-actions-deps group with 5 updates by @dependabot[bot] in #3531
• Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in #3536
• Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in #3577
• Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in #3581
• Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in #3589
• Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in #3596
• Bump the gradle-deps group with 3 updates by @dependabot[bot] in #3603
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in #3617
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in #3627
• Bump the gradle-deps group with 7 updates by @dependabot[bot] in #3646
• Bump the gradle-deps group with 2 updates by @dependabot[bot] in #3649
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in #3655
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in #3656
• Bump gradle/actions from 4 to 5 in the github-actions-deps group by @dependabot[bot] in #3667
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in #3666
• Bump the gradle-deps group with 9 updates by @dependabot[bot] in #3679
• Bump actions/upload-artifact from 4 to 5 in the github-actions-deps group by @dependabot[bot] in #3680
• Bump actions/checkout from 5 to 6 in the github-actions-deps group by @dependabot[bot] in #3694
• Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in #3695
• Bump the gradle-deps group with 4 updates by @dependabot[bot] in #3704
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in #3705
• Bump the gradle-deps group with 4 updates by @dependabot[bot] in #3712
• Bump the gradle-deps group with 7 updates by @dependabot[bot] in #3731
• Bump actions/upload-artifact from 6 to 7 in the github-actions-deps group by @dependabot[bot] in #3752
• Bump the gradle-deps group across 1 directory with 9 updates by @dependabot[bot] in #3756
• Bump the github-actions-deps group with 3 updates by @dependabot[bot] in #3798
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in #3797
• Bump the gradle-deps group with 3 updates by @dependabot[bot] in #3807
• Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in #3815
• Bump the gradle-deps group across 1 directory with 8 updates by @dependabot[bot] in #3818
• Bump actions/checkout from 6 to 7 in the github-actions-deps group by @dependabot[bot] in #3871
• Bump the gradle-deps group across 1 directory with 9 updates by @dependabot[bot] in #3872
• Migrate to Gradle Version Catalog by @wadoon in #3894

Other Changes

• Using semantic version (SemVer) scheme for KeY by @wadoon in #3523
• fixes Location#compareTo(Location) by @BookWood7th in #3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in #3521
• Missing project description for two sub-modules by @wadoon in #3528
• Re-enable sonarqube for quality assessment by @wadoon in #3488
• Also depend on checker-qual artifact by @wmdietl in #3535
• Added BoyerMoore.key by @TudorBalan in #3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in #3556
• Fix/Improve KeY example application by @samysweb in #3562
• Cleanup: Removal of key.api package by @wadoon in #3550
• Add documentation for soundDefaultContracts feature by @flo2702 in #3574
• Use a custom Github action for setting up the SMT solvers by @wadoon in #3569
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in #3579
• Warn on missing SMT solvers if flag is set by @wadoon in #3600
• Fix for a performance regression by @unp1 in #3607
• Fix Checker Framework Errors by @Drodt in #3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in #3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in #3613
• Remove duplicate NewDependingOn class by @Drodt in #3615
• Generalize Taclet Implementation by @Drodt in #3605
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in #3616
• Move Taclet matching infrastructure to ncore by @unp1 in #3608
• Using FlatLAF for a modern look and feel by @wadoon in #3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in #3624
• Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in #3626
• Test if matrix over modules are a good thing by @wadoon in #3622
• Cleanup: Use Standard Tech for Test Fixtures by @wadoon in #3551
• Remove unnecessary (and harmful) license plugin by @Drodt in #3628
• Reduce raw usage of classes by @Drodt in #3634
• Fix multiple SLF4J providers by @BookWood7th in #3639
• Indent switch expressions by @Drodt in #3636
• Translation of bitwise operators by @ChristianHein in #3172
• Throw an error when encountering an undefined rule set by @Drodt in #3644
• Preparation for generalizing rule indexing by @unp1 in #3620
• Improvements for AbbrevMap by @wadoon in #3647
• small fixes to datatype handling by @mattulbrich in #3661
• Improve error message in headless mode by @fynngodau in #3685
• Set version to 2.13.0-dev by @wadoon in #3689
• Generate easier POs for non-trivial diverges clauses by @Drodt in #3430
• (Re-)activating an ancient rule for the treatment of exactInstance of null by @mattulbrich in #3706
• Migrating to central portal from OSSRH, due to OSSRH shutdown in summer'25 by @wadoon in #3604
• Fix nullchecker by @Drodt in #3732
• Fix NPE in proof tree when using global filters by @flo2702 in #3755
• Refixing #3721: Starting KeY UI with local files by @mattulbrich in #3754
• Modularity for Proof Strategies by @Drodt in #3650
• Update and fix Broad Release Tests by @wadoon in #3703
• Support for TextBlockLiterals by @wadoon in #3796
• Record support by transformation by @wadoon in #3758
• Suppression of log for non-failing test classes by @wadoon in #3746
• Update function explanations to new syntax by @Drodt in #3811
• Update Gradle version to 9.5 and deprecated method replacements by @unp1 in #3813
• Remove codecov from CI by @wadoon in #3802
• Artifacts are now on mvn central by @wadoon in #3820
• Local performance improvements by @unp1 in #3824
• Improvements of Error Messages and Accurracy of Error Position Reporting by @unp1 in #3826
• Improve Update Simplification for Long Programs by @unp1 in #3828
• Deployment to Maven Central SNAPSHOT by @wadoon in #3819
• Optimize NonDuplicateEqApp-features by @unp1 in #3829
• Modularize KeY Grammar by @Drodt in #3822
• Make semicolon after rule optional by @Drodt in #3832
• Support co- and contravariant sorts by @Drodt in #3841
• Fix gradle task dependencies by @wadoon in #3853
• Remaining Changes for the KeY JSON-RPC API by @wadoon in #3849
• Revert "Create temporary PR body file" by @wadoon in #3852
• Taclet match dialog: collapse big matched terms; add an editor for SV fields by @unp1 in #3855
• Fix newline escape for Windows by @Drodt in #3856
• Further improvements on error message reporting by @unp1 in #3859
• Performance (5/5): operator-indexed parking of assumes-incomplete rule-app bases by @unp1 in #3838
• Performance (3/5): skip the checkPrefix prefix-walk when no transformer is present by @unp1 in #3836
• Performance (2/5): cut proof-search allocations + release the parser DFA cache by @unp1 in #3835
• Performance (1/5): Matching can now partially evaluate taclets by @unp1 in #3831
• Performance (4/5): reuse rule-app cost across re-expansion (+ age as a cost term) by @unp1 in #3837
• LogicPrinter: reduce per-subterm overhead and harden against unbalanced blocks by @unp1 in #3861
• Make proof-tree painting cheap on large proofs by @unp1 in #3863
• Fix intermittent key.core.testgen failures from SMT symbol-map race by @unp1 in #3862
• Regression tests for resolved parser/JML issues (#1119, #1536); pin #329 by @unp1 in #3868
• MetaSpace for documentation and origin by @wadoon in #3787
• Update the InfoTree component by @wadoon in #3786
• Report missing \endmodality at the modality opening; move source-location classes to ncore (#3867) by @unp1 in #3870
• Better ImmutableList by @wadoon in #3816
• Taclet match dialog: readable \assumes candidates and smarter window placement by @unp1 in #3882
• Performance Series 2 (1/5): Faster cost computation by skipping an unnecessary proof-history walk by @unp1 in #3874
• Performance Series 2 (2/5): Faster term equality modulo renaming via a hash pre-filter by @unp1 in #3875
• Performance Series 2 (3/5): Incremental taclet re-indexing for a single added taclet by @unp1 in #3876
• Performance Series 2 (5/5): Faster quantifier-instantiation heuristic, plus code cleanup by @unp1 in #3878
• Performance Series 2 (4/5): Lower memory for the per-goal rule-application queue by @unp1 in #3877
• Removal of proof_references and symbolic_execution modules by @wadoon in #3910
• Fix recent file menu; fix #3898 by @wadoon in #3909
• Add test for Java parsing coverage by @unp1 in #3916
• Support for multi-catch-clauses in try-statements by @wadoon in #3919
• Support for try-with-resources by reduction by @wadoon in #3918
• Remove proof-tree node border by @flo2702 in #3928

New Contributors

• @TudorBalan made their first contribution in #3558
• @frereit made their first contribution in #3568
• @fynngodau made their first contribution in #3685
• @PiIsRational made their first contribution in #3700

Full Changelog: KEY-2.12.3...KeY-3.0.0