diff --git a/README.md b/README.md index 30f7b75..c65a79f 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ ## Getting Started to Write An overview about some markdown (extension) is avaiable in `docs/howtodoc.md` or -http://key-project.org/docs/howtodoc/ +https://keyproject.github.io/key-docs/devel/howtodoc/ Webpages are determined by folder structure under `docs/`. Just create or change files within this folder. The top-level header is the title of this page in the 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) diff --git a/docs/user/quicktour/appendix.md b/docs/user/quicktour/appendix.md index 7e32486..007d084 100644 --- a/docs/user/quicktour/appendix.md +++ b/docs/user/quicktour/appendix.md @@ -478,10 +478,9 @@ Setting Up Own Projects {#app:configuringProjects} If not specified otherwise via a classpath directive, KeY includes a restricted set of signatures of classes and methods from the default standard library. The current set of classes can be found -at . +at . -For documentation on how to set up your own classpath, see -. +For documentation on how to set up your own classpath, see [Using the classpath directives in KeY](../Classpath.md). [^1]: Potential warnings can be safely ignored here. diff --git a/docs/workbench/Proof Scripts/index.md b/docs/workbench/Proof Scripts/index.md index c3a692f..6e7467b 100644 --- a/docs/workbench/Proof Scripts/index.md +++ b/docs/workbench/Proof Scripts/index.md @@ -4,7 +4,7 @@ To persist interactions performed during proof contsruction in KeY and to replay interactions, KeY allows users to use proof scripts. In this documentation the scripts that allow for branching statements are eplained. (see [Explanation -of linear scripts](https://key-project.org/docs/Proof%20Scripts/linearScripts) for the other version of scripts in KeY) +of linear scripts](./linearScripts.md) for the other version of scripts in KeY) The three main building blocks of the scripting language are mutators, control-flow structures, and selectors for proof goals. We describe the general concepts in the diff --git a/share/quicktour/tex/text/appendix.tex b/share/quicktour/tex/text/appendix.tex index f841938..5118dd3 100644 --- a/share/quicktour/tex/text/appendix.tex +++ b/share/quicktour/tex/text/appendix.tex @@ -481,9 +481,9 @@ \section{Setting Up Own Projects} If not specified otherwise via a classpath directive, \KeY\ includes a restricted set of signatures of classes and methods from the default -standard library. The current set of classes can be found at~\url{https://git.key-project.org/key-public/key/-/tree/stable/key/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux}. +standard library. The current set of classes can be found at~\url{https://github.com/KeYProject/key/tree/main/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux}. -For documentation on how to set up your own classpath, see \url{https://www.key-project.org/docs/Using\%20KeY/Classpath/}. +For documentation on how to set up your own classpath, see \url{https://keyproject.github.io/key-docs/user/Classpath/}. %%% Local Variables: