Release changes for 3.0.0

.github/workflows/nightlydeploy.yml

@@ -53,17 +53,17 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          gh release delete nightly --yes --cleanup-tag 
+          gh release delete KEY-3.0.0-rc --yes --cleanup-tag 
 
 
       - name: Create nightly release
         id: create_release
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          gh release create --generate-notes --title "Nightly Release" \
-             --prerelease --notes-start-tag KEY-2.12.3 \
-             nightly key.ui/build/libs/key-*-exe.jar key-javadoc.tar.xz
+          gh release create --generate-notes --title "KeY-3.0.0" \
+            --notes-start-tag KEY-2.12.3 \
+             KeY-3.0.0 key.ui/build/libs/key-*-exe.jar key-javadoc.tar.xz
 
 
       - name: Upload to MAVEN CENTRAL SNAPSHOT repository

LICENSE.TXT

@@ -3,7 +3,7 @@
        Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
                                Universitaet Koblenz-Landau, Germany
                                Chalmers University of Technology, Sweden
-       Copyright (C) 2011-2019 Karlsruhe Institute of Technology, Germany
+       Copyright (C) 2011-2026 Karlsruhe Institute of Technology, Germany
                                Technical University Darmstadt, Germany
                                Chalmers University of Technology, Sweden
 

README.md

@@ -6,20 +6,22 @@
 ![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Frepo1.maven.org%2Fmaven2%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20central)
 
 
-This repository is the home of the interactive theorem prover KeY for formal verification and analysis of Java programs. KeY comes as a standalone GUI application, which allows you to verify the functional correctness of Java programs with respect to formal specifications formulated in the Java Modeling Language JML. Moreover, KeY can also be used as a library e.g. for symbolic program execution, first order reasoning, or test case generation.
+This repository is the home of the interactive theorem prover KeY for formal verification and analysis of Java programs.
+KeY comes as a standalone GUI application, which allows you to verify the functional correctness of Java programs with
+respect to formal specifications formulated in the Java Modeling Language JML. Moreover, KeY can also be used as a
+library e.g. for symbolic program execution, first order reasoning, or test case generation.
 
 For more information, refer to
 
 * [The KeY homepage](https://key-project.org) 
 * [The KeY book](https://www.key-project.org/thebook2/)
-* [The KeY developer documentation](https://keyproject.github.io/key-docs/)
+* [The KeY documentation pages](https://keyproject.github.io/key-docs/)
 * KeY's success stories:
   * [Severe bug discovered in JDK sorting routine (TimSort)](http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/),  
   * [Verification of `java.util.IdentityHashMap`](https://doi.org/10.1007/978-3-031-07727-2_4),
   * [Google Award for analysing a bug in `LinkedList`](https://www.key-project.org/2023/07/23/cwi-researchers-win-google-award-for-finding-a-bug-in-javas-linkedlist-using-key/)
 
-The current version of KeY is 2.12.2, licensed under GPL v2.
-
+The current version of KeY is 3.0, licensed under GPL v2.
 
 Feel free to use the project templates to get started using KeY:
 * [For Verification Projects](https://github.com/KeYProject/verification-project-template)
@@ -30,7 +32,7 @@ Feel free to use the project templates to get started using KeY:
 
 * Hardware: >=2 GB RAM
 * Operating System: Linux/Unix, MacOSX, Windows
-* Java 17 or newer
+* Java 21 or newer
 * Optionally, KeY can make use of the following binaries:
   * SMT Solvers:
     * [Z3](https://github.com/Z3Prover/z3#z3)
@@ -87,17 +89,10 @@ Assuming you are in the directory of this README file, you can create a runnable
 
 # Developing KeY
 
-* Quality is automatically assessed using [SonarQube](https://sonarqube.org) on each pull request.
-  The results of the assessments (pass/fail) can be inspected in the checks section of the PR.
-
-  The rules and quality gate are maintained by Alexander Weigl
-  <weigl@kit.edu> currently.
-
-* More guideline and documentation for the KeY development can be found under
+Guidelines and documentation for the KeY development can be found under
 [key-docs](https://keyproject.github.io/key-docs/devel/).
 
 
-
 # Issues and Bug Reports
 
 * For bug reports, please use the [issue tracker](https://github.com/KeYProject/key/issues) or send a mail to support@key-project.org. 
@@ -106,7 +101,9 @@ Assuming you are in the directory of this README file, you can create a runnable
 
 # Contributing to KeY
 
-Feel free to submit [pull requests](https://github.com/KeYProject/key/pulls) via GitHub. Pull requests are assessed using automatic tests, formatting and static source checkers, as well as a manual review by one of the developers. More guidelines and documentation for the KeY development can be found under [key-docs](https://keyproject.github.io/key-docs/devel/).
+Feel free to submit [pull requests](https://github.com/KeYProject/key/pulls) via GitHub. Pull requests are assessed
+using automatic tests, formatting and static source checkers, as well as a manual review by one of the developers. More
+guidelines and documentation for the KeY development can be found under [key-docs](https://keyproject.github.io/key-docs/devel/).
 
 
 

build.gradle

@@ -19,8 +19,20 @@ plugins {
 
     // Plugin for publishing via the new Nexus API
     alias(libs.plugins.maven.publish) apply false
+
+    //alias(libs.plugins.license.report)
 }
 
+/* // required for generated the license report THIRD_PARTY_LICENSES.txt
+licenseReport {
+    unionParentPomLicenses = false
+    outputDir = layout.buildDirectory.dir("licenses").get().asFile
+    projects = [project] + project.subprojects
+    configurations = ['runtimeClasspath']
+    excludeOwnGroup = true
+    excludeBoms = false
+}
+*/
 
 // Configure this project for use inside IntelliJ:
 idea {
@@ -35,7 +47,7 @@ static def getDate() {
 }
 
 // The $BUILD_NUMBER is an environment variable set by Jenkins.
-def build = System.env.BUILD_NUMBER == null ? "-dev" : "-${System.env.BUILD_NUMBER}"
+def build = System.env.BUILD_NUMBER == null ? "" : "-${System.env.BUILD_NUMBER}"
 
 group = "org.key-project"
 version = "3.0.0$build"
@@ -46,6 +58,8 @@ subprojects {
     apply plugin: "idea"
     apply plugin: "eclipse"
 
+//    apply plugin: libs.plugins.license.report
+
     apply plugin: "com.diffplug.spotless"
     apply plugin: "org.checkerframework"
     apply plugin: "com.vanniktech.maven.publish"
@@ -62,6 +76,7 @@ subprojects {
     repositories {
         mavenCentral()
         //maven { url = "https://git.key-project.org/api/v4/projects/35/packages/maven/" }
+        //maven { url = "https://central.sonatype.com/repository/maven-snapshots/" }
     }
 
     dependencies {
@@ -293,7 +308,11 @@ subprojects {
 
         pom {
             name = project.name
-            description = project.description
+            afterEvaluate {
+                description = project.description
+                assert (project.description != null && project.description != "") : "Description of modules are required at maven-central"
+                print(project.description)
+            }
             url = 'https://key-project.org/'
 
             licenses {

gradle.properties

@@ -1 +1,4 @@
-org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8
+org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8
+
+# do not release automatically at Maven Central
+mavenCentralAutomaticPublishing=false

gradle/libs.versions.toml

@@ -23,7 +23,7 @@ stringtemplate = "4.3.4"
 
 # Java parsing and analysis
 javapoet = "1.13.0"
-javaparser = "3.28.0-K13.5"
+javaparser = "3.28.0-K13.6"
 truth = "1.4.5"
 
 # UI and CLI
@@ -98,3 +98,4 @@ spotless = { id = "com.diffplug.spotless", version.ref = "spotless" }
 checkerframework = { id = "org.checkerframework", version.ref = "checkerframework-gradle" }
 maven-publish = { id = "com.vanniktech.maven.publish", version.ref = "maven-publish" }
 shadow = { id = "com.gradleup.shadow", version.ref = "shadow" }
+license-report = { id = "com.github.jk1.dependency-license-report", version = "3.1.4" }

key.core.infflow/build.gradle

@@ -1,3 +1,4 @@
+description = "Information-Flow / Non-interference calculus for Java using the KeY theorem prover"
 
 
 dependencies {

key.core.wd/build.gradle

@@ -1,3 +1,6 @@
+description = "Well-defined calculus for JML specifciation and Java using the KeY theorem prover"
+
+
 dependencies {
     api(project(":key.core"))
 

key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java

@@ -5,8 +5,7 @@
 
 import java.io.*;
 import java.nio.charset.StandardCharsets;
-import java.nio.file.Files;
-import java.nio.file.Path;
+import java.nio.file.*;
 import java.util.*;
 
 import de.uka.ilkd.key.control.instantiation_model.TacletFindModel;
@@ -33,30 +32,44 @@ public class InstantiationFileHandler {
 
     private static Map<String, List<List<String>>> hm;
 
-    /// Finds the current place to store used instantiation. If there was a version switch
+    /// Finds the current place to store used instantiations. If there was a version change
     /// (the folder does not exist), this method tries to copy previous instantiations to
-    /// the new directory silently.
-    ///
-    /// It is guaranteed, that the folder exists.
+    /// the new directory silently. However, if both old and new instantiations exist, they are not
+    /// merge, i.e. only the new ones are used currently.
     private static Path getStoragePath() {
         Path cur = PathConfig.currentPaths.keyConfigDir.resolve("instantiations");
         if (Files.exists(cur)) {
+            /*
+             * At the moment, we do not merge when old and new instantiations are
+             * present. In the future, we could go one step further and try to merge.
+             */
             return cur;
         }
-
-        Path prev = PathConfig.previousPaths.keyConfigDir.resolve("instantiations");
+        // create the directory for storing instantiations
         try {
             Files.createDirectories(cur);
+        } catch (IOException e) {
+            LOGGER.warn("Could not create the instantiations folder {}", cur, e);
+        }
+
+        // Check if instantiations from older key version exist. If so, try to copy them over.
+        Path prev = PathConfig.previousPaths.keyConfigDir.resolve("instantiations");
+        if (Files.exists(prev)) {
             try (var files = Files.walk(prev)) {
                 files.forEach(path -> {
                     try {
-                        Files.copy(path, cur.resolve(path.relativize(prev)));
-                    } catch (IOException ignore) {
+                        Path target = cur.resolve(prev.relativize(path));
+                        // Do not overwrite existing file!
+                        if (!Files.exists(target)) {
+                            Files.copy(path, target);
+                        }
+                    } catch (IOException inner) {
+                        LOGGER.warn("Could not copy instantiation file {}", path, inner);
                     }
                 });
+            } catch (IOException e) {
+                LOGGER.warn("Could not copy instantiation files from {} to {}", prev, cur, e);
             }
-        } catch (IOException e) {
-            throw new RuntimeException(e);
         }
         return cur;
     }
@@ -82,9 +95,9 @@ private static void createHashMap() {
         hm = new TreeMap<>();
         try (var stream = Files.list(INSTANTIATION_DIR)) {
             // using a TreeMap here avoids non-determinsm introduce by the file system.
-            stream.forEach(file -> hm.put(file.toString(), null));
+            stream.forEach(file -> hm.put(file.getFileName().toString(), null));
         } catch (IOException e) {
-            LOGGER.warn("Could not read the instantions folder {}", INSTANTIATION_DIR, e);
+            LOGGER.warn("Could not read the instantiations folder {}", INSTANTIATION_DIR, e);
         }
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java

@@ -80,6 +80,7 @@ public class InitConfig {
 
     /** HashMap for quick lookups taclet name->taclet */
     private Map<Name, Taclet> activatedTacletCache = null;
+    private boolean defaultsComputed;
 
     /** the fileRepo which is responsible for consistency between source code and proof */
     private FileRepo fileRepo;
@@ -104,6 +105,9 @@ public InitConfig(Services services) {
     /// combines the found choices in KeY files, together with the current settings.
     /// The namespace of choices has to be filled.
     public void computeDefaults(ChoiceInformation ci) {
+        if (defaultsComputed) {
+            return;
+        }
         var currentDefaultChoices =
             ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices();
 
@@ -145,6 +149,8 @@ public void computeDefaults(ChoiceInformation ci) {
             }
             settings.getChoiceSettings().setDefaultChoices(defaults);
         }
+        activatedTacletCache = null;
+        defaultsComputed = true;
     }
 
     /**
@@ -203,6 +209,14 @@ public Map<Taclet, TacletBuilder<? extends Taclet>> getTaclet2Builder() {
     }
 
 
+    /**
+     * @return an immutable mapping from a category to its default choice
+     */
+    public @NonNull Map<String, Choice> getCategory2DefaultChoices() {
+        return Collections.unmodifiableMap(category2DefaultChoice);
+    }
+
+
     /**
      * sets the set of activated choices of this initial configuration. For categories without a
      * specified choice the default choice contained in category2DefaultChoice is added.
@@ -448,6 +462,7 @@ public InitConfig copyWithServices(Services services) {
         ic.header = header;
         ic.justifInfo = justifInfo.copy();
         ic.fileRepo = fileRepo; // TODO: copy instead? delete via dispose method?
+        ic.defaultsComputed = defaultsComputed;
         return ic;
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java

@@ -23,6 +23,7 @@
 import de.uka.ilkd.key.logic.label.OriginTermLabelFactory;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.logic.sort.GenericSort;
+import de.uka.ilkd.key.nparser.ChoiceInformation;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.JavaModel;
 import de.uka.ilkd.key.proof.Proof;
@@ -381,11 +382,14 @@ private void populateNamespaces(Proof proof) {
         }
     }
 
-    // what is the purpose of this method?
+    /**
+     * Updates the global settings the taclet options that declared in
+     * {@code optionDeclaration.key}.
+     * A proof created afterwards inherits these settings unless it overwrites it.
+     */
     private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig) {
-        // TODO: what does this actually do?
         ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().updateChoices(initConfig.choiceNS(),
-            false);
+            initConfig.getCategory2DefaultChoices(), false);
         return initConfig;
     }
 
@@ -494,7 +498,7 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException {
         var warnings = ic.getProfile()
                 .prepareInitConfig(ic, additionalProfileOptions);
         addWarnings(warnings);
-
+        ic.computeDefaults(new ChoiceInformation());
         return ic;
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java

@@ -256,7 +256,7 @@ public Path readBootClassPath() {
         if (!bootClassPathFile.isAbsolute()) {
             // convert to absolute by resolving against the parent path of the parsed file
             Path parentDirectory = file.file().getParent();
-            bootClassPathFile = parentDirectory.resolve(bootClassPathFile);
+            bootClassPathFile = parentDirectory.resolve(bootClassPathFile).normalize();
         }
         if (!Files.isDirectory(bootClassPathFile)) {
             // Report the missing directory at the \bootclasspath declaration in the .key file,
@@ -297,7 +297,7 @@ private static Location locationOrUndefined(ProblemInformation pi, String path)
             } else {
                 var f = Paths.get(normalizeStoredPath(cp));
                 if (!f.isAbsolute()) {
-                    f = parentDirectory.resolve(f);
+                    f = parentDirectory.resolve(f).normalize();
                 }
                 if (!Files.exists(f)) {
                     // Point at the \classpath declaration in the .key file instead of letting the
@@ -321,7 +321,7 @@ public Path readJavaPath() throws ProofInputException {
             if (!absFile.isAbsolute()) {
                 // convert to absolute by resolving against the parent path of the parsed file
                 Path parent = file.file().getParent();
-                absFile = parent.resolve(javaPath);
+                absFile = parent.resolve(javaPath).normalize();
             }
             if (!Files.exists(absFile)) {
                 throw new ProofInputException(String.format(