From 17f05178ccdcf2c60956170efbcd0dd207a0f53e Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 23 Aug 2023 09:51:00 +0200 Subject: [PATCH] Include changelog for 2.12 Co-Authored-By: Wolfram Pfeifer Co-Authored-By: Alexander Weigl --- docs/changelog.md | 217 +++++++++++++++++++++++++++++++++++++--------- 1 file changed, 174 insertions(+), 43 deletions(-) diff --git a/docs/changelog.md b/docs/changelog.md index 9e856c6..db367dd 100644 --- a/docs/changelog.md +++ b/docs/changelog.md @@ -1,48 +1,179 @@ # Changelog -## Upcoming: 2.12.0 (2023-08-02) - -### Core - -* **BREAK:** Minimum required Java version is 11. (!380) -* NEW: Floating point number support ([!403]) -* NEW: [Proof Slicing](user/ProofSlicing.md) system -* NEW: [Proof Caching](user/ProofCaching.md) system -* NEW: Java source validity is checked using javac ([!581]) -* IMP: Removal of the Eclipse Plugins. Eclipse support is now shipped in [keyclipse repository](https://git.key-project.org/key/keyclipse) (!390) -* IMP: Removal of `System.out/err` in favor for logging with SLF4J (!240) -* IMP: Translation of the last DL contracts to JML contracts. (!375) -* IMP: jdiv and jmod support in SMT translation via definitions -* IMP: support \old() in jml asserts ([!533]) -* FIX: Z3 counterexample generation works again ([!623]) -* FIX: Check for correct polarity when applying taclets ([!616]) -* Bring INVISMT to KeY; Refactors SolverTypes (!406) -* Performance: Switching sequents (!482) -* change SwitchToIf to create a if-else cascade (!444) -* More proof script commands: hide and unhide. (!486) -* Enables JavaDL data types in ghost and model fields (!469) -* insert jml assume and assert statements in the right order (!476) -* Performance: Autopilot ([!508]) -* Performance: Several memory leaks fixed ([!573]) - -### UI -* More functionality in statistics dialog -* Configurable look and feel ([!635]) -* Proof loading shows a progress bar ([!560]) - -### Development - -* New SMT solver configuration system ([!514], ...) -* Code style fixes ([!618], [!619]) -* Preparations for Gradle 8 ([!620]) -* Checkstyle updated to latest version ([!631]) -* Apply Spotless to code base (automatic formatting) ([!584]) -* JUnit 5 ([!489]) -* Externalization of Interaction Logging ([!500]) -* Fix comment attachment in recoder (!399) -* Restore RECODER-0.84 (!424) -* Update dependencies (!467) -* No dependencies as local jar files (!484) +## [2.12.0](https://github.com/KeYProject/key/releases/tag/KeY-2.12.0) (2023-08-18) + +### Breaking changes +* [The minimum required JDK version is set to 11.](https://git.key-project.org/key/key/-/merge_requests/380) +- 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](https://git.key-project.org/key/key/-/merge_requests/403) +* [Support for JML asserts/assumes as standalone construct (instead of transforming into blockcontracts)](https://git.key-project.org/key/key/-/merge_requests/494), [Support of \old() in JML asserts](https://git.key-project.org/key/key/-/merge_requests/533) +* [Support for JML math mode specifiers (and changed default semantics to spec_bigint_math)](https://github.com/KeYProject/key/pull/3014) +* [Proof Slicing](user/ProofSlicing.md) system ([#3026](https://github.com/KeYProject/key/pull/3026)) +* [Proof Caching](user/ProofCaching.md) system +* [Run the Javac compiler when loading Java code](https://git.key-project.org/key/key/-/merge_requests/581) +* Migration to GitHub + * [Files for Github Actions](https://git.key-project.org/key/key/-/merge_requests/634) + * [Add `merge_group` event to checks](https://github.com/KeYProject/key/pull/3060) + * Artiweb: [#3047](https://github.com/KeYProject/key/pull/3047), [#3097](https://github.com/KeYProject/key/pull/3097), [#3098](https://github.com/KeYProject/key/pull/3098), [#3101](https://github.com/KeYProject/key/pull/3101), [#3102](https://github.com/KeYProject/key/pull/3102), [#3103](https://github.com/KeYProject/key/pull/3103) + * [Upload HTML test report](https://github.com/KeYProject/key/pull/3010) + * [Dependabot](https://github.com/KeYProject/key/pull/3002) + +### Features + +* [Enable JavaDL data types in ghost and model fields](https://git.key-project.org/key/key/-/merge_requests/469) +* [Change SwitchToIf to create a if-else cascade](https://git.key-project.org/key/key/-/merge_requests/444) +* [More proof script commands: hide and unhide](https://git.key-project.org/key/key/-/merge_requests/486) +* [Logging via slf4j](https://git.key-project.org/key/key/-/merge_requests/240) +* [Suggested automation for seqPerm](https://git.key-project.org/key/key/-/merge_requests/531) +* [More descriptive names for result variables](https://git.key-project.org/key/key/-/merge_requests/542) +* [Implement some features of the jml assert wishlist](https://git.key-project.org/key/key/-/merge_requests/532) +* [ChoiceExpr: En-/Disabling taclets/goal templates using boolean expression](https://git.key-project.org/key/key/-/merge_requests/574) +* [New rules from the sorting case study](https://git.key-project.org/key/key/-/merge_requests/567) +* [Overflow checking](https://github.com/KeYProject/key/pull/3027) +* [Bring INVISMT to KeY; Refactors SolverTypes](https://git.key-project.org/key/key/-/merge_requests/406) +* [Redux additions](https://git.key-project.org/key/key/-/merge_requests/588) + +### UI/UX Improvements +* [Selection history (back + forward button)](https://github.com/KeYProject/key/pull/3006) +* [Generic undo button for user actions](https://github.com/KeYProject/key/pull/3009) +* [Expand oss nodes](https://github.com/KeYProject/key/pull/3061) +* [Allow user to select any installed LaF](https://github.com/KeYProject/key/pull/3038) +* [Un-clutter the context menus in the proof tree view](https://git.key-project.org/key/key/-/merge_requests/611) +* [Close more dialogs on escape press](https://git.key-project.org/key/key/-/merge_requests/571) +* [Replay progress display](https://git.key-project.org/key/key/-/merge_requests/560) +* [Improved taclet error reporting](https://git.key-project.org/key/key/-/merge_requests/603) +* [Immediately resize proof tree font](https://git.key-project.org/key/key/-/merge_requests/624) +* [Tooltip for the exloration status label](https://git.key-project.org/key/key/-/merge_requests/592) +* [Update log button, use Desktop.open instead of edit, fix an exception and log format on windows](https://git.key-project.org/key/key/-/merge_requests/610) +* [Report location on error in constant evaluation](https://github.com/KeYProject/key/pull/3025) +* [Report better error for missing model method]( https://github.com/KeYProject/key/pull/3041) +* [Proof tree view: Multiple small changes for readability](https://github.com/KeYProject/key/pull/3012) +* [Disable exploration tree updates when disabled](https://git.key-project.org/key/key/-/merge_requests/569) +* [Focus first cell in the taclet instantiation dialog on open](https://git.key-project.org/key/key/-/merge_requests/572) +* [Clipboard: Replace nbsp from html document selection with normal spaces](https://git.key-project.org/key/key/-/merge_requests/480) +* [Improve naming in recently used files dropdown](https://git.key-project.org/key/key/-/merge_requests/622) +### 🛠 Maintenance/Internal Changes + +* Logging + * [Logging cleanup](https://github.com/KeYProject/key/pull/3093) + * [Housekeeping: Logging](https://git.key-project.org/key/key/-/merge_requests/540) + +* Code formatting with spotless + * [Check formatting with Spotless](https://git.key-project.org/key/key/-/merge_requests/497) + * [Formatted rules](https://git.key-project.org/key/key/-/merge_requests/597) + * [Set an import order for Java code](https://github.com/KeYProject/key/pull/3094) + * [Apply Spotless to code base: Source code reformatting (no license headers)](https://git.key-project.org/key/key/-/merge_requests/584) + * [Spotless: Don't join manually split lines](https://git.key-project.org/key/key/-/merge_requests/586) + +* Code-Clean-Ups and Refactoring: + * [Replace the hardcoded SolverType classes by .props files](https://git.key-project.org/key/key/-/merge_requests/514) + * [Position information overhaul](https://github.com/KeYProject/key/pull/3049) + * [Remove ServiceLoaderUtil](https://git.key-project.org/key/key/-/merge_requests/470) + * [Remove last Eclipse files](https://git.key-project.org/key/key/-/merge_requests/471) + * [Code cleanup](https://github.com/KeYProject/key/pull/3064) + * [Miscellaneous cleanups (unused classes removed etc.)](https://github.com/KeYProject/key/pull/3044) + * [Removal of the Eclipse Plugins](https://git.key-project.org/key/key/-/merge_requests/390) + * [Remove sonarqube from readme](https://github.com/KeYProject/key/pull/3077) + * [Cleanup: Remove extension of CreatingASTVisitor by MergeRuleUtils.CollectLocationVariablesVisitor](https://git.key-project.org/key/key/-/merge_requests/529) + * [Some code cleanup](https://git.key-project.org/key/key/-/merge_requests/619) + * [Refactor Java formatter used in the sequent view](https://github.com/KeYProject/key/pull/3034) + * [Overhaul of the Configuration](https://github.com/KeYProject/key/pull/3031) + * [Add possibility to check for unsupported properties keys to SettingsConverter and clean up the class](https://git.key-project.org/key/key/-/merge_requests/638) + * [Removal of the Proof Collection Parser](https://github.com/KeYProject/key/pull/3030) + +* Dependencies + * [Recoder became part of this repo (Version 0.84 incl. KeY extensions)](https://git.key-project.org/key/key/-/merge_requests/424) + * [Update dependencies](https://git.key-project.org/key/key/-/merge_requests/467) + * [No dependencies as local jar files](https://git.key-project.org/key/key/-/merge_requests/484) + * [JUnit 5](https://git.key-project.org/key/key/-/merge_requests/489) + * [Update Checkstyle configuration to latest Checkstyle version](https://git.key-project.org/key/key/-/merge_requests/631) + * [Externalization of Interaction Logging](https://git.key-project.org/key/key/-/merge_requests/500) + * [Prepare build.gradle scripts for Gradle 8.0](https://git.key-project.org/key/key/-/merge_requests/620) + +* Performance + * [Performance when switching nodes](https://git.key-project.org/key/key/-/merge_requests/482) + * [Autopilot Performance: hasModality](https://git.key-project.org/key/key/-/merge_requests/508) + * [Performance: pause tree updates while executing "Set All Goals Below to XX"](https://git.key-project.org/key/key/-/merge_requests/528) + * [Avoid creating proof obligations in ProofManagementDialog](https://git.key-project.org/key/key/-/merge_requests/554) + +* Tests + * [JUnit XML files for optional-tests](https://github.com/KeYProject/key/pull/3096) + * [Add documentation for TestTacletEquality and update oracle](https://git.key-project.org/key/key/-/merge_requests/473) + * [Restore Information FlowTests](https://git.key-project.org/key/key/-/merge_requests/553) + * [Split `testRunAllProofs` into two tasks](https://git.key-project.org/key/key/-/merge_requests/559) + * [Disable proof_references + symbolic_execution](https://git.key-project.org/key/key/-/merge_requests/589) + +* Misc + * [Small tweaks to proof script engine](https://github.com/KeYProject/key/pull/3020) + * [Reducing the binary filesize by only including the necessary example files](https://git.key-project.org/key/key/-/merge_requests/626) + * [Improve smt solver checking on windows](https://git.key-project.org/key/key/-/merge_requests/609) + * [Translating DL contracts to JML](https://git.key-project.org/key/key/-/merge_requests/375) + * [Read `\profile` and `\settings` once](https://github.com/KeYProject/key/pull/3007) + * [Stop the message about java_profile.jfr](https://git.key-project.org/key/key/-/merge_requests/590) + * [Suppress logback message before configuration](https://git.key-project.org/key/key/-/merge_requests/591) + * [Support for jdiv and jmod in SMT translation via definitions](https://git.key-project.org/key/key/-/merge_requests/547) + * [Add gen folder to gitignore](https://git.key-project.org/key/key/-/merge_requests/598) + * [Add Task runWithProfiler to execute key.ui with the Java Flight Recoder](https://git.key-project.org/key/key/-/merge_requests/504) + * [Load some (old) proofs with wrong/missing instantiations of \assumes in taclet app](https://git.key-project.org/key/key/-/merge_requests/516) + * [Specialized version of RuleContext::getText in TextualJMLAssertStatement::getClauseText](https://git.key-project.org/key/key/-/merge_requests/479) + * [Multiplication for rule costs](https://git.key-project.org/key/key/-/merge_requests/541) + +### 🐛 Bug Fixes + +* [Bug fixes from the IdentityHashMap case study](https://git.key-project.org/key/key/-/merge_requests/499) +* [Remove highlighting artifacts in SequentView with Unicode symbols enabled](https://git.key-project.org/key/key/-/merge_requests/595) +* [Avoid tooltip NPE for incomplete proof nodes](https://github.com/KeYProject/key/pull/3037) +* [Always load correct example on double click](https://git.key-project.org/key/key/-/merge_requests/632) +* [TokenMgrErr in issue dialogs](https://git.key-project.org/key/key/-/merge_requests/633) +* [Fix exception when parsing unknown source name in BuildingException](https://git.key-project.org/key/key/-/merge_requests/570) +* [Solve missing plugin in shadowJar by adding `mergeServiceFiles()`](https://git.key-project.org/key/key/-/merge_requests/545) +* [Fix Z3 counterexample generation](https://git.key-project.org/key/key/-/merge_requests/623) +* [Fix three memory leaks](https://git.key-project.org/key/key/-/merge_requests/573) +* [Keep original PositionInfo in ForToWhileTransformation](https://git.key-project.org/key/key/-/merge_requests/628) +* [Check for correct polarity when applying taclets](https://git.key-project.org/key/key/-/merge_requests/616) +* [Add triggers to textual representations of taclets](https://git.key-project.org/key/key/-/merge_requests/600) +* [Allow declaration of function symbols in custom key file and to use them in JML via \dl](https://git.key-project.org/key/key/-/merge_requests/602) +* [Fix leftover files that are not formatted properly](https://git.key-project.org/key/key/-/merge_requests/604) +* [Fix loop in strategy](https://git.key-project.org/key/key/-/merge_requests/129) +* [Fix PosInProgram](https://git.key-project.org/key/key/-/merge_requests/621) +* [Fix file filter for .proof.gz files](https://git.key-project.org/key/key/-/merge_requests/536) +* [Fixed rule "wellFormedStoreObjectEQ"](https://git.key-project.org/key/key/-/merge_requests/526) +* [Resolve "Taclet leaves a broken tree after failing to apply"](https://git.key-project.org/key/key/-/merge_requests/492) +* [Fix potential stack overflow in ExplorationStepsList](https://git.key-project.org/key/key/-/merge_requests/510) +* [Show message of the chained cause of the exception in IssueDialog](https://git.key-project.org/key/key/-/merge_requests/515) +* [Ensure that the condition of a JML assert statement is always a formula](https://git.key-project.org/key/key/-/merge_requests/530) +* [Fix widening casts and boxing of extension primitive types like bigint](https://git.key-project.org/key/key/-/merge_requests/583) +* [Fix construction of Javac issue dialog](https://github.com/KeYProject/key/pull/3008) +* [Fix handling of multiline log messages]( https://github.com/KeYProject/key/pull/3033) +* [Fix javacc deprecation warning]( https://github.com/KeYProject/key/pull/3016) +* [Fix ProofTreeView NPE](https://github.com/KeYProject/key/pull/3070) +* [Fix program element printing in proof saver](https://github.com/KeYProject/key/pull/3073) +* [Fix some positions being offset](https://github.com/KeYProject/key/pull/3084) +* [Fix type of `Long.MIN_VALUE` and `Long.MAX_VALUE`](https://github.com/KeYProject/key/pull/3100) +* [Activate Z3 if no other SMT solver is configured](https://github.com/KeYProject/key/pull/3048) +* [Register modifier when parsing JML spec](https://github.com/KeYProject/key/pull/3040) +* [Fix set statements (allow expressions on lhs, e.g. for array and field access)](https://git.key-project.org/key/key/-/merge_requests/566) +* [Fix IllegalArgumentException being thrown from IssueDialog](https://git.key-project.org/key/key/-/merge_requests/485) +* [Insert JML assume and assert statements in the right order](https://git.key-project.org/key/key/-/merge_requests/476) +* [Make AbbrevMap::getTerm fulfill its contract and prevent a NPE](https://git.key-project.org/key/key/-/merge_requests/481) +* [A collection for some (straight forward) of the SonarQube reliability bugs](https://git.key-project.org/key/key/-/merge_requests/618) +* [Remove space from taclet proof save file name](https://git.key-project.org/key/key/-/merge_requests/568) +* [Resolve "Parsing exception: undeclared variable in an assignable declaration"](https://git.key-project.org/key/key/-/merge_requests/506) +* [Fix for heap/permissions/threads example](https://git.key-project.org/key/key/-/merge_requests/527) +* [Repairing JML interpretation of equality on floats and doubles.](https://git.key-project.org/key/key/-/merge_requests/524) + +* Further bug fixes: [#1664](https://git.key-project.org/key/key/-/merge_requests/474), [#1658](https://git.key-project.org/key/key/-/merge_requests/491), [#1652](https://git.key-project.org/key/key/-/merge_requests/495), [#1679](https://git.key-project.org/key/key/-/merge_requests/503), [#1681, #1682](https://git.key-project.org/key/key/-/merge_requests/507), [#1678](https://git.key-project.org/key/key/-/merge_requests/521), [#1685](https://git.key-project.org/key/key/-/merge_requests/512), [#1690](https://git.key-project.org/key/key/-/merge_requests/517), [#1706](https://git.key-project.org/key/key/-/merge_requests/538), [#1709](https://git.key-project.org/key/key/-/merge_requests/539), [#1684](https://git.key-project.org/key/key/-/merge_requests/511), [#1711](https://git.key-project.org/key/key/-/merge_requests/549), [#1707](https://git.key-project.org/key/key/-/merge_requests/601), [#1723](https://git.key-project.org/key/key/-/merge_requests/587), [#1598](https://git.key-project.org/key/key/-/merge_requests/513), [#3035](https://github.com/KeYProject/key/pull/3045) + +--- +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 ## 2.10.0 (2021-12-23)