key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3516
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3517
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• Bump the gradle-deps group with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3527
• Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3526
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Bump the github-actions-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3531
• Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3536
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3577
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3581
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3589
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3596
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3603
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3617
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608
• Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624
• Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626
• Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622
• Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3627
• Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628
• Disable relative path test on Windows by @wadoon in https://github.com/KeYProject/key/pull/3629
• Fix SMT ApplyAction not pruning when undoing by @BookWood7th in https://github.com/KeYProject/key/pull/3606
• Reduce raw usage of classes by @Drodt in https://github.com/KeYProject/key/pull/3634
• Fix multiple SLF4J providers by @BookWood7th in https://github.com/KeYProject/key/pull/3639
• Indent switch expressions by @Drodt in https://github.com/KeYProject/key/pull/3636
• Translation of bitwise operators by @ChristianHein in https://github.com/KeYProject/key/pull/3172
• Throw an error when encountering an undefined rule set by @Drodt in https://github.com/KeYProject/key/pull/3644
• Refactoring context menus of sequent views by @wadoon in https://github.com/KeYProject/key/pull/3641
• Bump the gradle-deps group with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3646
• Bump the gradle-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3649
• Introducing some structure for model method bodies by @mattulbrich in https://github.com/KeYProject/key/pull/3571
• Fix NPE using KeY command line interface caused by Java NIO by @wadoon in https://github.com/KeYProject/key/pull/3643
• Preparation for generalizing rule indexing by @unp1 in https://github.com/KeYProject/key/pull/3620
• FIX: URGENT: Changes in Gradle 9 results into non-execution of custom test tasks. by @wadoon in https://github.com/KeYProject/key/pull/3653
• fix css for sequentview syntaxhighlightning by @wadoon in https://github.com/KeYProject/key/pull/3645
• Improvements for AbbrevMap by @wadoon in https://github.com/KeYProject/key/pull/3647

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 6 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3516
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3517
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• Bump the gradle-deps group with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3527
• Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3526
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Bump the github-actions-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3531
• Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3536
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3577
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3581
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3589
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3596
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3603
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3617
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608
• Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624
• Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626
• Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622
• Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3627
• Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628
• Disable relative path test on Windows by @wadoon in https://github.com/KeYProject/key/pull/3629
• Fix SMT ApplyAction not pruning when undoing by @BookWood7th in https://github.com/KeYProject/key/pull/3606
• Reduce raw usage of classes by @Drodt in https://github.com/KeYProject/key/pull/3634
• Fix multiple SLF4J providers by @BookWood7th in https://github.com/KeYProject/key/pull/3639
• Indent switch expressions by @Drodt in https://github.com/KeYProject/key/pull/3636
• Translation of bitwise operators by @ChristianHein in https://github.com/KeYProject/key/pull/3172
• Throw an error when encountering an undefined rule set by @Drodt in https://github.com/KeYProject/key/pull/3644
• Refactoring context menus of sequent views by @wadoon in https://github.com/KeYProject/key/pull/3641
• Bump the gradle-deps group with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3646
• Bump the gradle-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3649
• Introducing some structure for model method bodies by @mattulbrich in https://github.com/KeYProject/key/pull/3571
• Fix NPE using KeY command line interface caused by Java NIO by @wadoon in https://github.com/KeYProject/key/pull/3643
• Preparation for generalizing rule indexing by @unp1 in https://github.com/KeYProject/key/pull/3620
• FIX: URGENT: Changes in Gradle 9 results into non-execution of custom test tasks. by @wadoon in https://github.com/KeYProject/key/pull/3653
• fix css for sequentview syntaxhighlightning by @wadoon in https://github.com/KeYProject/key/pull/3645

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 6 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3516
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3517
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• Bump the gradle-deps group with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3527
• Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3526
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Bump the github-actions-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3531
• Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3536
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3577
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3581
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3589
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3596
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3603
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3617
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608
• Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624
• Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626
• Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622
• Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3627
• Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628
• Disable relative path test on Windows by @wadoon in https://github.com/KeYProject/key/pull/3629
• Fix SMT ApplyAction not pruning when undoing by @BookWood7th in https://github.com/KeYProject/key/pull/3606
• Reduce raw usage of classes by @Drodt in https://github.com/KeYProject/key/pull/3634
• Fix multiple SLF4J providers by @BookWood7th in https://github.com/KeYProject/key/pull/3639
• Indent switch expressions by @Drodt in https://github.com/KeYProject/key/pull/3636
• Translation of bitwise operators by @ChristianHein in https://github.com/KeYProject/key/pull/3172
• Throw an error when encountering an undefined rule set by @Drodt in https://github.com/KeYProject/key/pull/3644
• Refactoring context menus of sequent views by @wadoon in https://github.com/KeYProject/key/pull/3641
• Bump the gradle-deps group with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3646
• Bump the gradle-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3649

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 7 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3516
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3517
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• Bump the gradle-deps group with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3527
• Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3526
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Bump the github-actions-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3531
• Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3536
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3577
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3581
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3589
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3596
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3603
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3617
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608
• Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624
• Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626
• Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622
• Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3627
• Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628
• Disable relative path test on Windows by @wadoon in https://github.com/KeYProject/key/pull/3629
• Fix SMT ApplyAction not pruning when undoing by @BookWood7th in https://github.com/KeYProject/key/pull/3606
• Reduce raw usage of classes by @Drodt in https://github.com/KeYProject/key/pull/3634
• Fix multiple SLF4J providers by @BookWood7th in https://github.com/KeYProject/key/pull/3639
• Indent switch expressions by @Drodt in https://github.com/KeYProject/key/pull/3636

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 7 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3516
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3517
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• Bump the gradle-deps group with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3527
• Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3526
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Bump the github-actions-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3531
• Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3536
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3577
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3581
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3589
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3596
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3603
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3617
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608
• Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624
• Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626
• Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622
• Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3627
• Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628
• Disable relative path test on Windows by @wadoon in https://github.com/KeYProject/key/pull/3629
• Fix SMT ApplyAction not pruning when undoing by @BookWood7th in https://github.com/KeYProject/key/pull/3606
• Reduce raw usage of classes by @Drodt in https://github.com/KeYProject/key/pull/3634

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 7 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3516
• Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3517
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• Bump the gradle-deps group with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3527
• Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3526
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Bump the github-actions-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3531
• Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3536
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3577
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3581
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3589
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3596
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3603
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3617
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608
• Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624
• Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626
• Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622
• Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551
• Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3627
• Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628
• Disable relative path test on Windows by @wadoon in https://github.com/KeYProject/key/pull/3629
• Fix SMT ApplyAction not pruning when undoing by @BookWood7th in https://github.com/KeYProject/key/pull/3606

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 7 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608
• Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624
• Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626
• Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622
• Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551
• Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 8 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608
• Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599
• Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 8 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616
• Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 8 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615
• Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618
• Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605
• fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619
• Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 9 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607
• Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609
• Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610
• Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612
• Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613
• Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 9 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592
• Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600
• Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514
• Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578
• Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 9 months ago

key - Nightly Release

What's Changed

Breaking Changes 🗲

• Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 ### Other Changes
• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579
• SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 10 months ago

key - Nightly Release

What's Changed

Other Changes

• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598
• Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594
• Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 10 months ago

key - Nightly Release

What's Changed

Other Changes

• Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522
• Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523
• Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520
• fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519
• RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521
• Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528
• Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488
• Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525
• Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529
• Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533
• Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535
• Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540
• Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537
• Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558
• repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556
• Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562
• Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550
• fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560
• Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566
• Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559
• Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543
• Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574
• highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573
• Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495
• Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569
• fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583
• Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593
• Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598

New Contributors

• @TudorBalan made their first contribution in https://github.com/KeYProject/key/pull/3558
• @frereit made their first contribution in https://github.com/KeYProject/key/pull/3568

Full Changelog: https://github.com/KeYProject/key/compare/KEY-2.12.3...nightly

- Java
Published by github-actions[bot] 10 months ago

key - KeY-2.12.3 (2024-09-08)

What's Changed

• Update LICENSE.TXT to reflect GPL-2.0-only by @FliegendeWurst in https://github.com/KeYProject/key/pull/3223
• Post-Release 2.12.0: Backport bug fixes into main by @wadoon in https://github.com/KeYProject/key/pull/3242
• Update BSH dependency of recoder by @wadoon in https://github.com/KeYProject/key/pull/3250
• Post-Release: Backport Deployment Changes to KeY by @wadoon in https://github.com/KeYProject/key/pull/3246
• Post-Release 2.12.0: Java and Version by @wadoon in https://github.com/KeYProject/key/pull/3241
• Applying Java 17 refactorings by @wadoon in https://github.com/KeYProject/key/pull/3252
• Fix dependency issue in SMT translation by @FliegendeWurst in https://github.com/KeYProject/key/pull/3275
• UI: avoid freeze when applying SMT results by @FliegendeWurst in https://github.com/KeYProject/key/pull/3255
• Stop automode or exit on SIGINT by @FliegendeWurst in https://github.com/KeYProject/key/pull/3249
• updating README.md by @mattulbrich in https://github.com/KeYProject/key/pull/3288
• Problem statements in KeY file can now also be a (semi-)sequent by @wadoon in https://github.com/KeYProject/key/pull/3283
• Further Refactorings for Java 17+ by @wadoon in https://github.com/KeYProject/key/pull/3264
• SMT: add Z3_QF variant by @FliegendeWurst in https://github.com/KeYProject/key/pull/3287
• Fix for issue #3158 by @unp1 in https://github.com/KeYProject/key/pull/3224
• Some general minor code quality improvements by @unp1 in https://github.com/KeYProject/key/pull/3293
• Update beanshell to 2.0b6 by @unp1 in https://github.com/KeYProject/key/pull/3294
• Backport of KEY-2.12.1 into main by @wadoon in https://github.com/KeYProject/key/pull/3296
• Fix wrong quicksave failed warning by @unp1 in https://github.com/KeYProject/key/pull/3298
• Fix for issue #3286: Parsing of rule display names that contain spaces in origin labels by @unp1 in https://github.com/KeYProject/key/pull/3306
• Restore TermImpl to package private and strengthen immutability of term and sorts by @unp1 in https://github.com/KeYProject/key/pull/3304
• Fix Issue #3186: Model method looses nullability modifiers by @unp1 in https://github.com/KeYProject/key/pull/3307
• Revert lazy term index updates by @unp1 in https://github.com/KeYProject/key/pull/3312
• Allow origin labels to be switched off completely by @unp1 in https://github.com/KeYProject/key/pull/3316
• Proof Slicing: make dependency tracking optional by @FliegendeWurst in https://github.com/KeYProject/key/pull/3309
• replace JSR305 annotations with JSpecify by @wadoon in https://github.com/KeYProject/key/pull/3290
• A heap indicator in KeY's status bar by @wadoon in https://github.com/KeYProject/key/pull/3325
• fix ClassCastException in LogicPrinter by @wadoon in https://github.com/KeYProject/key/pull/3326
• Fix JavaDoc errors by @unp1 in https://github.com/KeYProject/key/pull/3329
• Fix broken addLabel Method in TermBuilder by @Drodt in https://github.com/KeYProject/key/pull/3331
• Heap status extension: proper max. value of progress bar by @FliegendeWurst in https://github.com/KeYProject/key/pull/3332
• Fix all warnings reported by ./gradlew javadoc by @unp1 in https://github.com/KeYProject/key/pull/3330
• Method names should not be created via VariableRenamer by @unp1 in https://github.com/KeYProject/key/pull/3231
• Create a basic CONTRIBUTING.md by @FliegendeWurst in https://github.com/KeYProject/key/pull/3333
• Print real condition in if labels by @FliegendeWurst in https://github.com/KeYProject/key/pull/3222
• Fix consistency of proof status and tasktree icon by @unp1 in https://github.com/KeYProject/key/pull/3344
• Show notification after running macro by @FliegendeWurst in https://github.com/KeYProject/key/pull/3269
• Update to Java 21 Runtime for Testing by @wadoon in https://github.com/KeYProject/key/pull/3282
• Add help buttons to extension settings by @FliegendeWurst in https://github.com/KeYProject/key/pull/3348
• suggesting a pull-request-template. by @mattulbrich in https://github.com/KeYProject/key/pull/3018
• A new grammar for configuration by @wadoon in https://github.com/KeYProject/key/pull/3099
• Fix (for issue #3347) that node selection gets forgotten when switching between proofs by @unp1 in https://github.com/KeYProject/key/pull/3349
• Re-enable check for non-unique taclet names and remove two taclet duplicates by @unp1 in https://github.com/KeYProject/key/pull/3359
• Avoid name clashes in rule applyUpdateOnRigid by @tobias-rnh in https://github.com/KeYProject/key/pull/3355
• Handle bound variables in SMT unknown translation by @FliegendeWurst in https://github.com/KeYProject/key/pull/3263
• Fix update of proof tree in case of filter changes (fixes #3367) by @unp1 in https://github.com/KeYProject/key/pull/3368
• Configurable enabled keys for JML condition evaluation by @wadoon in https://github.com/KeYProject/key/pull/3373
• Get rid of experimental flag using more fine-grained flags by @wadoon in https://github.com/KeYProject/key/pull/3370
• ADTs for KeY by @wadoon in https://github.com/KeYProject/key/pull/3161
• Renovation: package.html to package-info.java by @wadoon in https://github.com/KeYProject/key/pull/3381
• Fix passing of warnings by @wadoon in https://github.com/KeYProject/key/pull/3302
• Proof caching: use dependency graph to increase hit rate by @FliegendeWurst in https://github.com/KeYProject/key/pull/3305
• Always sort extension actions in context submenus (+bugfix to allow disabling extensions) by @FliegendeWurst in https://github.com/KeYProject/key/pull/3392
• Update README.md (license date and Java version) by @WolframPfeifer in https://github.com/KeYProject/key/pull/3412
• Activate the OverloadedOperatorHandler.java for Sequence datatype by @wadoon in https://github.com/KeYProject/key/pull/3398
• Solved an issue with row/column numbers in JML Parser by @LennartKleinwort in https://github.com/KeYProject/key/pull/3419
• Fix error handling for unknown sorts by @MarcoScaletta in https://github.com/KeYProject/key/pull/3428
• Hackathon: error reporting by @FliegendeWurst in https://github.com/KeYProject/key/pull/3426
• Fix position info for equality expr errors by @FliegendeWurst in https://github.com/KeYProject/key/pull/3429
• Add ADT Destructors by @Drodt in https://github.com/KeYProject/key/pull/3420
• JML enabled keys indicator for the Status Line by @wadoon in https://github.com/KeYProject/key/pull/3374
• fixes #1533 by @JonasKlamroth in https://github.com/KeYProject/key/pull/3423
• Hackeython smt mod by @BookWood7th in https://github.com/KeYProject/key/pull/3418
• added checkbox to disable example loader directly in dialog by @JonasKlamroth in https://github.com/KeYProject/key/pull/3424
• Generalizing Logic Data Structures by @Drodt in https://github.com/KeYProject/key/pull/3357
• Fix startup crash if ~/.key/colors.json is not present by @FliegendeWurst in https://github.com/KeYProject/key/pull/3439
• fix smt solver downloader script by @wadoon in https://github.com/KeYProject/key/pull/3445
• Update broken link in README.md by @FliegendeWurst in https://github.com/KeYProject/key/pull/3444
• Update pullrequesttemplate.md by @mattulbrich in https://github.com/KeYProject/key/pull/3446
• Immutable and valid JML set statement by @wadoon in https://github.com/KeYProject/key/pull/3400
• Combine equalsMod... methods by @tobias-rnh in https://github.com/KeYProject/key/pull/3386
• Introducing a new function symbol seqUpd by @mattulbrich in https://github.com/KeYProject/key/pull/3385
• Cleanup of declaration of taclet options by @WolframPfeifer in https://github.com/KeYProject/key/pull/3408
• Boyer Moore Majority Vote by @mattulbrich in https://github.com/KeYProject/key/pull/3454
• Hackeython/error reporting by @mattulbrich in https://github.com/KeYProject/key/pull/3432
• Nicer error message for parse errors by @FliegendeWurst in https://github.com/KeYProject/key/pull/3417
• Fixes a StackOverflow when pretty printing a taclet by @unp1 in https://github.com/KeYProject/key/pull/3453
• Fix newnames handling for new local vars by @FliegendeWurst in https://github.com/KeYProject/key/pull/3438
• Prevent Dependency PO generation for void methods by @Drodt in https://github.com/KeYProject/key/pull/3422
• Update dependabot configuration by @wadoon in https://github.com/KeYProject/key/pull/3447
• Add key features for the FM tutorial by @wadoon in https://github.com/KeYProject/key/pull/3460
• Fixed the path-to-smt-solver bug in windows by @vb213 in https://github.com/KeYProject/key/pull/3434
• Support for JML\TYPE by @flo2702 in https://github.com/KeYProject/key/pull/3465
• Basic Nullness Checker configuration by @wmdietl in https://github.com/KeYProject/key/pull/3183
• Nullness Type System activated for key.ncore by @wadoon in https://github.com/KeYProject/key/pull/3468
• Renovation of PO loading by @wadoon in https://github.com/KeYProject/key/pull/3379
• Fix checkstyle workflow by @Drodt in https://github.com/KeYProject/key/pull/3471
• Generalize ParsableVariable and Schemavariables by @Drodt in https://github.com/KeYProject/key/pull/3436
• Removal of JUnit4 by @wadoon in https://github.com/KeYProject/key/pull/3462
• Allow "\seq()" and "\locset()" in JML by @mattulbrich in https://github.com/KeYProject/key/pull/3476
• Introduce JML aliases of frame conditions for better tool compatibility by @mi-ki in https://github.com/KeYProject/key/pull/3365
• Fix loading of closed proofs (GUI threw error) by @unp1 in https://github.com/KeYProject/key/pull/3479
• Fix loading of taclet proof obligations (issue #3477) by @unp1 in https://github.com/KeYProject/key/pull/3481
• RuleCommand can now deal with rules that have schema variables for logical variables by @mattulbrich in https://github.com/KeYProject/key/pull/3482
• Additional rule for sequences: Swap of sequence is a permutation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3485
• Hackeython unknown methods by @flo2702 in https://github.com/KeYProject/key/pull/3431
• Update Github Action for Gradle by @unp1 in https://github.com/KeYProject/key/pull/3480
• Fix overflow checking by @WolframPfeifer in https://github.com/KeYProject/key/pull/3353
• Fixed operator replacements in WD taclets after changes in PR #3436 by @mi-ki in https://github.com/KeYProject/key/pull/3484
• Realize generic navigation structure by @Drodt in https://github.com/KeYProject/key/pull/3472
• Overflow follow up fix by @WolframPfeifer in https://github.com/KeYProject/key/pull/3490
• More general equalsModProperty by @tobias-rnh in https://github.com/KeYProject/key/pull/3459
• saving proofs for sequent problems by @mattulbrich in https://github.com/KeYProject/key/pull/3496
• Map with new equalities by @tobias-rnh in https://github.com/KeYProject/key/pull/3486
• Remove Ctrl+C handling, see #3456 by @wadoon in https://github.com/KeYProject/key/pull/3499
• HacKeYthon: Improved Taclet Options by @tobias-rnh in https://github.com/KeYProject/key/pull/3433
• Fix for the LoopInvariantConfigurationDialog by @unp1 in https://github.com/KeYProject/key/pull/3377
• Revert "Fix CurrentGoalView highlights not being removed" by @mattulbrich in https://github.com/KeYProject/key/pull/3391
• Fix for #3501: Decrease log level of duplicate sort warnings by @WolframPfeifer in https://github.com/KeYProject/key/pull/3505
• Repairing the NonNull checker framework exception by @mattulbrich in https://github.com/KeYProject/key/pull/3507
• repairing heatmap updates for inner nodes by @mattulbrich in https://github.com/KeYProject/key/pull/3506
• Fix copyright notice by @flo2702 in https://github.com/KeYProject/key/pull/3508
• Fix for visual bug with overlapping/unreadable text in color settings by @WolframPfeifer in https://github.com/KeYProject/key/pull/3509
• Option to disable ProofTree tooltips, render them lazily by @WolframPfeifer in https://github.com/KeYProject/key/pull/3510

New Contributors

• @tobias-rnh made their first contribution in https://github.com/KeYProject/key/pull/3355
• @LennartKleinwort made their first contribution in https://github.com/KeYProject/key/pull/3419
• @MarcoScaletta made their first contribution in https://github.com/KeYProject/key/pull/3428
• @JonasKlamroth made their first contribution in https://github.com/KeYProject/key/pull/3423
• @BookWood7th made their first contribution in https://github.com/KeYProject/key/pull/3418
• @vb213 made their first contribution in https://github.com/KeYProject/key/pull/3434
• @wmdietl made their first contribution in https://github.com/KeYProject/key/pull/3183

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.12.2...KEY-2.12.3

- Java
Published by wadoon over 1 year ago

key - Nightly Release

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.4.0...nightly

- Java
Published by github-actions[bot] almost 2 years ago

key - Nightly Release

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.4.0...nightly

- Java
Published by github-actions[bot] about 2 years ago

key - Nightly Release

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.4.0...nightly

- Java
Published by github-actions[bot] about 2 years ago

key - KeY-2.12.2 (2023-11-10)

This release contains bug fixes and performance enhancements.

Changes

Performance:

• Z3 is now configurable to use the QF (quantifier-free) theory for problems without quantifiers.

Bug Fixes:

• The pretty printer no longer throws a ClassCastException when printing taclets using schema variables of an array type.
• Nullable and non-null modifiers attached to model methods are no longer lost.
• Term rule indices are now always up-to-date, preventing potential prover crashes.
• The counter-example dialog no longer freezes the GUI, if the example generation fails.
• The actual proof status and proof status icon in the task overview are now consistent after pruning without requiring a manual refresh.

- Java
Published by unp1 over 2 years ago

key - KeY-2.12.1 (2023-10-13)

Changes

Bug fixes

• SMT solvers are properly terminated on timeout
• Proof Macro statistics are kept visible and only count the newly applied rules
• Stop button is disabled after use, re-enabled after stop completes (this is to avoid double activation)
• Fully disable origin tracking if it is disabled
• Proof slicing works even if a cut introduced no new formulas in any branch
• When marking goal(s) as interactive/automatic, proof tree no longer loses expansion state
• Fix proof tree behaviour when toggling goals
• Fix branch selection in caching
• Fix gradle detection of git branch
• Fix unit test
• Fix environments not disposed in tests, keep strategy info visible after applying
• Proof macro: record statistics correctly
• Fix: KeY files with errors cannot be edited

- Java
Published by wadoon over 2 years ago

key - Nightly Release

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.4.0...nightly

- Java
Published by github-actions[bot] over 2 years ago

key - Nightly Release

What's Changed

• Fix NPE when no look and feel is configured by @FliegendeWurst in https://github.com/KeYProject/key/pull/3005
• Install SMT solvers for CI testing by @wadoon in https://github.com/KeYProject/key/pull/3001
• Fix branch name in Checkstyle script by @FliegendeWurst in https://github.com/KeYProject/key/pull/3015
• Update issue templates by @WolframPfeifer in https://github.com/KeYProject/key/pull/3004
• Fix use of unsupported string templates by @ChristianHein in https://github.com/KeYProject/key/pull/3011
• Update tests.yml by @wadoon in https://github.com/KeYProject/key/pull/3017
• Spec math mode by @jwiesler in https://github.com/KeYProject/key/pull/3014
• Fix construction of Javac issue dialog by @FliegendeWurst in https://github.com/KeYProject/key/pull/3008
• Report location on error in constant evaluation by @FliegendeWurst in https://github.com/KeYProject/key/pull/3025
• Draft: Fix javacc deprecation warning by @jwiesler in https://github.com/KeYProject/key/pull/3016
• Small tweaks to proof script engine by @mattulbrich in https://github.com/KeYProject/key/pull/3020
• Fix handling of multiline log messages by @FliegendeWurst in https://github.com/KeYProject/key/pull/3033
• Proof tree view: Multiple small changes for readability by @jwiesler in https://github.com/KeYProject/key/pull/3012
• New .git-blame-ignore-revs after history rewrite by @FliegendeWurst in https://github.com/KeYProject/key/pull/3036
• Avoid tooltip NPE for incomplete proof nodes by @FliegendeWurst in https://github.com/KeYProject/key/pull/3037
• Upload HTML test report by @wadoon in https://github.com/KeYProject/key/pull/3010
• Activate Z3 if no other SMT solver is configured by @FliegendeWurst in https://github.com/KeYProject/key/pull/3048
• Re-enable previously disabled tests by @FliegendeWurst in https://github.com/KeYProject/key/pull/3043
• Create dependabot.yml by @wadoon in https://github.com/KeYProject/key/pull/3002
• Bump org.junit.jupiter:junit-jupiter-params from 5.8.2 to 5.9.2 by @dependabot in https://github.com/KeYProject/key/pull/3051
• Bump org.junit.jupiter:junit-jupiter-engine from 5.8.2 to 5.9.2 by @dependabot in https://github.com/KeYProject/key/pull/3050
• Selection history (back + forward button) by @FliegendeWurst in https://github.com/KeYProject/key/pull/3006
• Artiweb comment workflow by @jwiesler in https://github.com/KeYProject/key/pull/3047
• Report better error for missing model method by @FliegendeWurst in https://github.com/KeYProject/key/pull/3041
• Miscellaneous cleanups (unused classes removed etc.) by @FliegendeWurst in https://github.com/KeYProject/key/pull/3044
• Fix #3035 by @jwiesler in https://github.com/KeYProject/key/pull/3045
• Add merge_group event to checks by @wadoon in https://github.com/KeYProject/key/pull/3060
• Bump org.slf4j:slf4j-api from 1.7.32 to 2.0.6 by @dependabot in https://github.com/KeYProject/key/pull/3052
• Bump com.diffplug.spotless from 6.11.0 to 6.16.0 by @dependabot in https://github.com/KeYProject/key/pull/3056
• Bump org.antlr:antlr-runtime from 3.5.2 to 3.5.3 by @dependabot in https://github.com/KeYProject/key/pull/3053
• Bump org.sonarqube from 3.3 to 4.0.0.2929 by @dependabot in https://github.com/KeYProject/key/pull/3054
• Allow user to select any installed LaF by @FliegendeWurst in https://github.com/KeYProject/key/pull/3038
• Register modifier when parsing JML spec by @FliegendeWurst in https://github.com/KeYProject/key/pull/3040
• Bump ch.qos.logback:logback-classic from 1.2.10 to 1.4.5 by @dependabot in https://github.com/KeYProject/key/pull/3055
• Formatter by @jwiesler in https://github.com/KeYProject/key/pull/3034
• Read \profile and \settings once (fixes #1738) by @FliegendeWurst in https://github.com/KeYProject/key/pull/3007
• Position information overhaul by @jwiesler in https://github.com/KeYProject/key/pull/3049
• Bump org.junit.vintage:junit-vintage-engine from 5.8.2 to 5.9.2 by @dependabot in https://github.com/KeYProject/key/pull/3069
• Bump org.antlr:antlr4 from 4.9.3 to 4.12.0 by @dependabot in https://github.com/KeYProject/key/pull/3067
• Bump org.antlr:antlr from 3.5.2 to 3.5.3 by @dependabot in https://github.com/KeYProject/key/pull/3065
• Enabling Java 17 for unit-tests by @wadoon in https://github.com/KeYProject/key/pull/3039
• Fix ProofTreeView NPE by @jwiesler in https://github.com/KeYProject/key/pull/3070
• Fix program element printing in proof saver by @FliegendeWurst in https://github.com/KeYProject/key/pull/3073
• Generic undo button for user actions by @FliegendeWurst in https://github.com/KeYProject/key/pull/3009
• Remove sonarqube from readme by @jwiesler in https://github.com/KeYProject/key/pull/3077
• Proof slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3026
• Expand oss nodes by @jwiesler in https://github.com/KeYProject/key/pull/3061
• Bump org.junit.jupiter:junit-jupiter-api from 5.8.2 to 5.9.2 by @dependabot in https://github.com/KeYProject/key/pull/3082
• Bump ch.qos.logback:logback-classic from 1.4.5 to 1.4.6 by @dependabot in https://github.com/KeYProject/key/pull/3079
• Bump org.ow2.asm:asm from 4.1 to 9.4 by @dependabot in https://github.com/KeYProject/key/pull/3080
• Overflow checking by @jwiesler in https://github.com/KeYProject/key/pull/3027
• Bump org.ow2.asm:asm from 9.4 to 9.5 by @dependabot in https://github.com/KeYProject/key/pull/3089
• Bump org.slf4j:slf4j-api from 2.0.6 to 2.0.7 by @dependabot in https://github.com/KeYProject/key/pull/3088
• Logging cleanup by @jwiesler in https://github.com/KeYProject/key/pull/3093
• Fix some positions being offset by @jwiesler in https://github.com/KeYProject/key/pull/3084
• Bump com.github.johnrengelman.shadow from 7.1.0 to 8.1.1 by @dependabot in https://github.com/KeYProject/key/pull/3090
• set an import order for Java code by @wadoon in https://github.com/KeYProject/key/pull/3094
• JUnit XML files for optional-tests by @wadoon in https://github.com/KeYProject/key/pull/3096
• Update of the test oracles files of key.core.symbolic_execution by @wadoon in https://github.com/KeYProject/key/pull/3095
• Better artiweb comment workflow by @jwiesler in https://github.com/KeYProject/key/pull/3097
• Code cleanup by @jwiesler in https://github.com/KeYProject/key/pull/3064
• Artiweb workflow fix by @jwiesler in https://github.com/KeYProject/key/pull/3098
• Fix type of Long.MIN_VALUE and Long.MAX_VALUE by @ChristianHein in https://github.com/KeYProject/key/pull/3100
• Artiweb workflow fix by @jwiesler in https://github.com/KeYProject/key/pull/3101
• Artiweb workflows by @jwiesler in https://github.com/KeYProject/key/pull/3102
• Artiweb by @jwiesler in https://github.com/KeYProject/key/pull/3103
• Removal of the Proof Collection Parser by @wadoon in https://github.com/KeYProject/key/pull/3030
• Fix comment author and nicer message by @jwiesler in https://github.com/KeYProject/key/pull/3104
• Overhaul of the Configuration by @wadoon in https://github.com/KeYProject/key/pull/3031

New Contributors

• @ChristianHein made their first contribution in https://github.com/KeYProject/key/pull/3011

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.10.0...nightly

- Java
Published by github-actions[bot] over 2 years ago

key - KeY-2.12.0 (2023-08-18)

Changes

Breaking changes

• The minimum required JDK version is set to 11.
• This release contains breaking changes for the reloading of older proofs:
  • Integers in specifications are now considered as unbounded (i.e. \bigint, math mode specifiers can be used to deviate from the default).
  • The list of rule sets used by the One-Step-Simplifier has changed.
  • JML assertions are handled as a standalone construct and not as a block contract anymore.

Highlights

• Support for floating points
• Support for JML asserts/assumes as standalone construct (instead of transforming into blockcontracts), Support of \old() in JML asserts
• Support for JML math mode specifiers (and changed default semantics to specbigintmath)

• Migration to Github

  • Files for Github Actions
  • Add merge_group event to checks
  • Artiweb: #3047, #3097, #3098, #3101, #3102, #3103
  • Upload HTML test report
  • Dependabot

• Proof slicing extension

• Run the Javac compiler when loading Java code

Features

• Enable JavaDL data types in ghost and model fields
• Change SwitchToIf to create a if-else cascade
• More proof script commands: hide and unhide
• Logging via slf4j
• Suggested automation for seqPerm
• More descriptive names for result variables
• Implement some features of the jml assert wishlist
• ChoiceExpr: En-/Disabling taclets/goal templates using boolean expression
• New rules from the sorting case study
• Overflow checking
• Bring INVISMT to KeY; Refactors SolverTypes
• Redux additions

UI/UX Improvements

• Selection history (back + forward button)
• Generic undo button for user actions
• Expand oss nodes
• Allow user to select any installed LaF
• Un-clutter the context menus in the proof tree view
• Close more dialogs on escape press
• Replay progress display
• Improved taclet error reporting
• Immediately resize proof tree font
• Tooltip for the exloration status label
• Update log button, use Desktop.open instead of edit, fix an exception and log format on windows
• Report location on error in constant evaluation
• Report better error for missing model method
• Proof tree view: Multiple small changes for readability
• Disable exploration tree updates when disabled
• Focus first cell in the taclet instantiation dialog on open
• Clipboard: Replace nbsp from html document selection with normal spaces

• Improve naming in recently used files dropdown

  🛠 Maintenance/Internal Changes

• Logging

  • Logging cleanup
  • Housekeeping: Logging

• Code formatting with spotless

  • Check formatting with Spotless
  • Formatted rules
  • Set an import order for Java code
  • Apply Spotless to code base: Source code reformatting (no license headers)
  • Spotless: Don't join manually split lines

• Code-Clean-Ups and Refactoring:

  • Replace the hardcoded SolverType classes by .props files
  • Position information overhaul
  • Remove ServiceLoaderUtil
  • Remove last Eclipse files
  • Code cleanup
  • Miscellaneous cleanups (unused classes removed etc.)
  • Removal of the Eclipse Plugins
  • Remove sonarqube from readme
  • Cleanup: Remove extension of CreatingASTVisitor by MergeRuleUtils.CollectLocationVariablesVisitor
  • Some code cleanup
  • Refactor Java formatter used in the sequent view
  • Overhaul of the Configuration
  • Add possibility to check for unsupported properties keys to SettingsConverter and clean up the class
  • Removal of the Proof Collection Parser

• Dependencies

  • Recoder became part of this repo (Version 0.84 incl. KeY extensions)
  • Update dependencies
  • No dependencies as local jar files
  • JUnit 5
  • Update Checkstyle configuration to latest Checkstyle version
  • Externalization of Interaction Logging
  • Prepare build.gradle scripts for Gradle 8.0

• Performance

  • Performance when switching nodes
  • Autopilot Performance: hasModality
  • Performance: pause tree updates while executing "Set All Goals Below to XX"
  • Avoid creating proof obligations in ProofManagementDialog

• Tests

  • JUnit XML files for optional-tests
  • Add documentation for TestTacletEquality and update oracle
  • Restore Information FlowTests
  • Split testRunAllProofs into two tasks
  • Disable proofreferences + symbolicexecution

• Misc

  • Small tweaks to proof script engine
  • Reducing the binary filesize by only including the necessary example files
  • Improve smt solver checking on windows
  • Translating DL contracts to JML
  • Read \profile and \settings once
  • Stop the message about java_profile.jfr
  • Suppress logback message before configuration
  • Support for jdiv and jmod in SMT translation via definitions
  • Add gen folder to gitignore
  • Add Task runWithProfiler to execute key.ui with the Java Flight Recoder
  • Load some (old) proofs with wrong/missing instantiations of \assumes in taclet app
  • Specialized version of RuleContext::getText in TextualJMLAssertStatement::getClauseText
  • Multiplication for rule costs

🐛 Bug Fixes

• Bug fixes from the IdentityHashMap case study
• Remove highlighting artifacts in SequentView with Unicode symbols enabled
• Avoid tooltip NPE for incomplete proof nodes
• Always load correct example on double click
• TokenMgrErr in issue dialogs
• Fix exception when parsing unknown source name in BuildingException
• Solve missing plugin in shadowJar by adding mergeServiceFiles()
• Fix Z3 counterexample generation
• Fix three memory leaks
• Keep original PositionInfo in ForToWhileTransformation
• Check for correct polarity when applying taclets
• Add triggers to textual representations of taclets
• Allow declaration of function symbols in custom key file and to use them in JML via \dl
• Fix leftover files that are not formatted properly
• Fix loop in strategy
• Fix PosInProgram
• Fix file filter for .proof.gz files
• Fixed rule "wellFormedStoreObjectEQ"
• Resolve "Taclet leaves a broken tree after failing to apply"
• Fix potential stack overflow in ExplorationStepsList
• Show message of the chained cause of the exception in IssueDialog
• Ensure that the condition of a JML assert statement is always a formula
• Fix widening casts and boxing of extension primitive types like bigint
• Fix construction of Javac issue dialog
• Fix handling of multiline log messages
• Fix javacc deprecation warning
• Fix ProofTreeView NPE
• Fix program element printing in proof saver
• Fix some positions being offset
• Fix type of Long.MIN_VALUE and Long.MAX_VALUE
• Activate Z3 if no other SMT solver is configured
• Register modifier when parsing JML spec
• Fix set statements (allow expressions on lhs, e.g. for array and field access)
• Fix IllegalArgumentException being thrown from IssueDialog
• Insert JML assume and assert statements in the right order
• Make AbbrevMap::getTerm fulfill its contract and prevent a NPE
• A collection for some (straight forward) of the SonarQube reliability bugs
• Remove space from taclet proof save file name
• Resolve "Parsing exception: undeclared variable in an assignable declaration"
• Fix for heap/permissions/threads example

• Repairing JML interpretation of equality on floats and doubles.

• Further bug fixes: #1664, #1658, #1652, #1679, #1681, #1682, #1678, #1685, #1690, #1706, #1709, #1684, #1711, #1707, #1723, #1598, #3035

---

We like to thank our contributors for this release, namely:

Alicia Appelhagen, Richard Bubel, Lukas Grätz, Christian Hein, Arne Keller, Michael Kirsten, Florian Lanzinger, Wolfram Pfeifer, Mike Schwörer, Benjamin Takacs, Samuel Teuber, Mattias Ulbrich, Alexander Weigl, Julian Wiesler

- Java
Published by wadoon over 2 years ago

key - KeY-2.6.2 (2017-04-13)

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.6.1...KeY-2.6.2

- Java
Published by wadoon about 3 years ago

key - KeY-2.6.1 (2017-01-31)

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.6.0...KeY-2.6.1

- Java
Published by wadoon about 3 years ago

key - KeY-2.6.0 (2016-12-22)

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.4.0...KeY-2.6.0

- Java
Published by wadoon about 3 years ago

key - KeY-2.4.1 (2015-02-18)

Nothing known.

- Java
Published by wadoon about 3 years ago

key - KeY-2.4.0 (2015-02-17)

• Information flow reasoning
• Full support for symbolic execution with bitwise operations
• Improved test case generation
• Improved user interface
• Support for CVC4 SMT solver backend

- Java
Published by wadoon about 3 years ago

key - KeY-2.2.3 (2014-10-06)

• Fix concurrency issue introduced in 2.2.2

- Java
Published by wadoon about 3 years ago

key - KeY-2.2.2 (2014-07-11)

• Support for CVC3 version 2.4.1 SMT backend
• Bug fixes

- Java
Published by wadoon about 3 years ago

key - KeY-2.2.1 (2014-05-27)

• Test case generation using bounded SMT (requires Z3, OpenJML)
• Bug fixes

- Java
Published by wadoon about 3 years ago

key - KeY-2.2.0 (2014-04-29)

• Counter example generation using bounded SMT (requires Z3)
• Increased JML support / JML extensions
  • block contracts (extension) / assert statements
  • \min and \max numerical quantifiers
  • changed default semantics of signals_only to include unchecked exceptions
  • model methods (new implementation)
  • old clause (variable binder in contract)
  • nearly everything parseable
• Verification of a large class of recursive methods
  • generalized variants to all ordered sets
• Proof obligations for specification well-definedness
• Term labels
• Rule triggers (extended taclet syntax)
• More efficient handling of heap disjointness and heap selects
• Improved reasoning about bounded sums/products
• User Interfaces
  • rule focus for inner nodes
  • improved search
  • detailed proof statistics
  • auto save and quick save features
  • keyboard shortcuts
• Reduced memory footprint
• A lot of bug fixes
• Java 8 compatibility
• Re-implemented .key parser

- Java
Published by wadoon about 3 years ago

key - KeY-2.0.2 (2013-09-19)

• Support for latest versions of Z3 and CVC3
• Windows 8 compatibility
• Fix a soundness issue with types and heap access
• Various bug fixes

- Java
Published by wadoon about 3 years ago

key - KeY-2.0.1 (2013-06-19)

• Bug fixes
  • Incompleteness with Java integer arithmetics
  • Command line mode fixes
  • various other

- Java
Published by wadoon about 3 years ago

key - KeY-2.0.0 (2013-04-18)

• New explicit heap modeling
  • Data types for location sets and heaps
  • The heap is now a special (local) variable
  • Dynamic frames
  • JML extension for dynamic frame specification
  • Re-implementation of JavaCard transactions
• Verification of (primitive) recursive methods
• Sequence ADT
• Nearly complete JML support
  • model fields and methods
  • initially clauses and class axioms
  • measured_by clauses
  • accessible clauses
  • sum and product comprehension
  • the \bigint type, mixed integer semantics
  • weak purity by default
  • reachability predicate
  • \index and \values keywords for enhanced for-loops
• Escape to dynamic logic from within JML
• MonKeY batch mode
• GUI changes
  • new dialog to enter invariants interactively
  • search in sequents and proof trees
  • logical symbols in Unicode
• Runnable from command line without windowing system
• Improved integration of SMT solvers
  • SMT-LIB 2.0 backend interface
  • possible to run multiple solvers in parallel
  • support for integer division (Z3 only)
• > 150 bug fixes
• Discontinued features
  • RTSJ support
  • Test case generation
  • OCL
  • Proof reuse

- Java
Published by wadoon about 3 years ago

key - KeY-1.6.5 (2013-01-23)

• Minor bugfixes
• Java 7 compatibility

- Java
Published by wadoon about 3 years ago

key - KeY-1.6.0 (2010-10-06)

• Support for Strings
• Enhanced JML support
• Improved integration of external SMT solvers
• Improved "verification-based testing" mechanism
• Real Time Java (RTSJ) calculus
• GUI improvements
• Various bugfixes

- Java
Published by wadoon about 3 years ago

key - KeY-1.4.0 (2009-03-25)

• Unified proof obligation framework
  • sharing of proof obligations across different specification languages
  • unified API for adding new proof obligations
  • same GUI elements used for all specification languages
  • more elegant translation of \old, @pre-like constructs
• Improved JavaCard DL Specification interface
  • specification of DL invariants
• Rewrite of JML front-end
  • ghost variables/fields and JML set statement
  • non_null by default
  • \old in loop invariants supported
  • \object_creation(type) in JML assignable clauses
• New standalone OCL front-end
  • discontinued support for Borland Together integration
• Java language support enhancements:
  • enum types (partially)
  • inner and anonymous classes
  • enhanced for loop
  • variable method arguments
  • covariant method signature
• Generation of JML specifications
• Strictly pure queries can be pushed directly into an update
• Stable proof loading and saving
• Classpath directive
• various bugfixes

- Java
Published by wadoon about 3 years ago

key - KeY-1.2.0 (2007-11-30)

• significantly improved proof strategies wrt. quantifier treatment and arithmetics
• improved proof tree view, i.e.
  • hiding of closed subtrees
  • hiding of intermediate proof steps
  • search in proof tree
• improved proof saving and loading
• includes alpha version of the visual debugger
• various bugfixes

- Java
Published by wadoon about 3 years ago

key - KeY-2.10.0 (2021-12-23)

Core

• IMP: New SMT translation (!312), rework of the SMT communication (!381), and smaller fixes (!394)
• IMP: Renovating the KeY parser (!278)
• IMP: Rewrite of the JML parser in ANTLR (!306) with better exception message (!376)
• IMP: JML-Extension: Assert/Assume and *_free for block contracts (!342)
• FIX: Comment attachment in recoder (!399, !401)
• FIX: Collision of auxiliary contract (!396)
• FIX: Path handling of key files (!395)
• FIX: Pruning in closed branches looses rules (!388, #1480)
• FIX: Repaired file information if a directory is opened in KeY (!386, #1530)
• FIX: Proof loading in the CLI (!385)
• FIX: Invalid URLs under Windows (#1504, !264)
• FIX: lost error messages due to MalformedURLException (!290, #1529)
• FIX: catch headless to make key --auto runnable again (!382)
• FIX: \singleton of a non-location (e.g., \singleton(3)) now raises an error (!377)
• FIX: Completeness gap for array types (!367, #1566)
• FIX: add loop scope unwind (!326)

UI

• IMP: A better dialog for warnings (!374)
• IMP: Performance tuning and fixes for ProofTree (!391)
• IMP: Enables selection of proof in Proof Differences view (!256)
• IMP: Better SourceView Tooltip (!379)
• IMP: Add setting to disable load examples dialog window (!368)
• IMP: Enable syntax highlighting for JML starting with annotation markers (!325)
• FIX: make proof to load from bundle selectable (!237)
• FIX: Escaping comma when saving bookmarked filenames of KeYFileChooser (!387, #1551)
• FIX: make exception dialog able to show files in Jar files (!383)
• FIX: Resolve "SMT Option GUI throws NPE on startup" (!373)

Development

• Enabling of SonarQube in Merge Requests (!323, !378)
• Dependency fixes for Gradle 7 (!372)

We like to thank all the contributor to this release:

Alexander Weigl, Alicia Appelhagen, Benjamin Takacs, Florian Lanzinger, Jonas Schiffl, Julian Wiesler, Lukas Grätz, Mattias Ulbrich, Michael Kirsten, Richard Bubel, Wolfram Pfeifer

- Java
Published by wadoon about 3 years ago

key - 2.8.0 (2020-12-01)

Logic

• NEW: bsum taclets (!96)
• NEW: Taclets for more flexible handling of observer depency (!177)
• NEW: Loop contracts improvements (!188)
• NEW: Loop scopes: a new rule for proving loop invaraints (!313, !326)
• NEW: Support for Annotation Marker in JML (!308)
• NEW: created new file intDiv.key for newly added taclets concerning (!182, !171, !180, !157, !152, !144, !141, !135, !98)
• NEW: SMT preparation macro (!165)
• NEW: Completion Scopes (!305)
• FIX: Bugfixing handling of program variables of type "any" and parsing (!133)
• NEW: \infinite_uniton(int x; x >= 0; this[x]) is now available in binder syntax: (\infinite_uniton int x; x >= 0; this[x]). Old form is deprecated and will be removed in later versions. (!132)
• NEW: Adding "System.arraycopy" with contract to JavaRedux (!137)
• NEW: Explizit excption for nested updates (allowed in the KeY book, unsupported by implementation) (!319)
• FIX: Speed up in saving proofs (!120)
• FIX: Incompleteness issue when rewite taclet was applied and the goaltemplate… (!119)
• NEW: Loop contract (!?, !73)
• NEW: Loading and Storing proofs with compression (gzip) (!12)
• NEW: Saving of proofs (incl. dependening resources) into one file (zip) called "proof bundle" (!237)
• FIX: Fix of inner blocks (!82)
• FIX: KeY read files character-wise, now the file content is cached (!XXX)
• More jml synonyms (!85)
• FIX: user-provided notes are saved within the proof file (!304)
• FIX: Origin labels for user interactions could not be parsed
• FIX: Method signature resolve in JML expressions (!309)

UI

• NEW: Unifying and polishing the user interface (!123):
  • KeY uses a docking framework, including storable/loadable layouts (!189)
  • The settings are concentrated inside one dialog (!189, !266)
  • Adaptable colors and key strokes (!189, !236, !254)
  • Adaptable clutter rules (!7)
  • Key based navigation within the proof tree view (!198)
  • FIX: Handling of regex in search (!199)
  • NEW: Icons !227
• NEW: Heatmaps: Coloring formulae on the sequent based on their change activity (!38, !140)
• NEW: Saving of proof bundles (!148, !310)
• NEW: View of the current source code marking executed parts. (!99, !260, !263, !267, !325)
• NEW: GUI Extension inferface: You can easily plugin new GUI elements.
• NEW: Origin labels tracks the origin of formulae within a sequence (!122, !248)
• NEW: Intraction logging (HacKeYthon'18) brings logging of user interaction with exports to Proof Scripts (!84)
• NEW: Proof exploration
• NEW: Favourites in file dialogs (!252)
• NEW: License dialog (!253)
• NEW: View for proof differences based on formula distance matching (!255)
• NEW: Schiffl's search filter (!4)
• NEW: Pre-select previous selected contract in ProofManagementDialog (!287)
• FIX: Parsing of char, integer and long literals (!9, #1446, !214, !196)
• FIX: Collision of heatmap and search colors (!178)
• FIX: Slightly less confusing presentation of SMT solver results (!160)
• FIX: Cluttering with the status line (!244)
• NEW: Allow macro application via keyboard shortcut from tree (!268)
• NEW: Open Java files without considering a classpath (!243)

Scripts

• NEW: Rewrite command (!51)
• FIX: Several fixes and breaking changes: (!153, !146, !145)
• NEW: Improvements to the proof scripts (!314)

Environment

• NEW: Gradle became build tool (!179, !205, !208, !209, !280)
  • Changes to the test infrastructure (!196)
  • Export of maven dependecies
  • New distribution formats: either a FatJar or zip file
• NEW: Quality assessment via sonarqube and sonarcloud (!323)
• Java 11 ready (!47)
  • remove of JavaFX dependencies (!95)
• Integrate tests for well-definedness checks (!87 )

Eclipse

• Support of Eclipse PHOTON (!74)

Seveal small and large bug fixes:

(!331, !297, !296, !293,!290, !288, !286, !284, !277, !276, !273, !272, !271, !270, !265, !264, !234, !228, !227, !225, !224, !222, !219, !213, !212, !209, !208, !205, !203, !201, !200, !199, !192, !190, !173, !170, !167, !163, !162, !158, !156, !154, !153, !151, !146, !145, !139, !136, !133, !131, !119, !117, !108, !99, !92, !83, !82, !81, !78, !77, !75, !73, !71, !70, !69, !68, !67, !66, !65, !58, !52, !47, !46, !45, !40, !39, !37, !33, !31, !30, !24, !23, !22, !14, !13, !10, !9, !8, !7, !3, !2)

We like to thank all the contributor to this release:

Alexander Weigl, Carsten Csiky, Dominic Steinhöfel, Florian Lanzinger, Hans-Dieter Hiep, Jelle Kübler, Jonas Schiffl, Lukas Grätz, Lulu Luong, Mattias Ulbrich, Michael Kirsten, Mihai Herda, Peter Schmitt, Richard Bubel, Sarah Grebing, Wolfram Pfeifer

- Java
Published by wadoon about 3 years ago

key - KeY-2.6.3 (2017-10-11)

Full Changelog: https://github.com/KeYProject/key/compare/KeY-2.6.2...KeY-2.6.3

- Java
Published by wadoon about 3 years ago