Applying Java 17 refactorings (#3252)

Applies refactorings after the switch to Java 17 for after #3241.

Including:

* Transform immutable data classes to Java records
* Rewrite `instanceof` and casts to Pattern expressions
* Use `.toList()` instead of `.collect(Collectors.toList)`
* Use Text Block Literals (`""" ... """`) on large strings instead of
concatenation cascades.

Author: wadoon

build.gradle

@@ -21,7 +21,7 @@ plugins {
     // id "com.github.ben-manes.versions" version "0.39.0"
 
     // Code formatting
-    id "com.diffplug.spotless" version "6.16.0"
+    id "com.diffplug.spotless" version "6.20.0"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -335,7 +335,10 @@ subprojects {
             toggleOffOn()
 
             removeUnusedImports()
-            eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml")
+            /* At the moment, we have to ensure that version 4.22 of the eclipse formatter is run, since newer versions
+             * of the formatter crash in SymbolicExecutionTreeBuilder (seems to be a but in the formatter)!
+             */
+            eclipse("4.22").configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml")
             trimTrailingWhitespace()        // not sure how to set this in the xml file ...
             //googleJavaFormat().aosp().reflowLongStrings()
 

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java

@@ -65,9 +65,8 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                         }
                     }
                 }
-                if (found instanceof PartialInvAxiom) {
+                if (found instanceof PartialInvAxiom axiom) {
                     // Invariant was applied
-                    PartialInvAxiom axiom = (PartialInvAxiom) found;
                     DefaultProofReference<ClassInvariant> reference =
                         new DefaultProofReference<>(IProofReference.USE_INVARIANT,
                             node, axiom.getInv());

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java

@@ -23,9 +23,7 @@ public class ContractProofReferencesAnalyst implements IProofReferencesAnalyst {
      */
     @Override
     public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
-        if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp) {
-            AbstractContractRuleApp contractRuleApp =
-                (AbstractContractRuleApp) node.getAppliedRuleApp();
+        if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp contractRuleApp) {
             DefaultProofReference<Contract> reference = new DefaultProofReference<>(
                 IProofReference.USE_CONTRACT, node, contractRuleApp.getInstantiation());
             LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java

@@ -26,8 +26,7 @@ public class MethodBodyExpandProofReferencesAnalyst implements IProofReferencesA
     public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
         if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
             NodeInfo info = node.getNodeInfo();
-            if (info.getActiveStatement() instanceof MethodBodyStatement) {
-                MethodBodyStatement mbs = (MethodBodyStatement) info.getActiveStatement();
+            if (info.getActiveStatement() instanceof MethodBodyStatement mbs) {
                 IProgramMethod pm = mbs.getProgramMethod(services);
                 DefaultProofReference<IProgramMethod> reference =
                     new DefaultProofReference<>(IProofReference.INLINE_METHOD, node,

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java

@@ -55,8 +55,7 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                         new LinkedHashSet<>();
                     result.add(reference);
                     return result;
-                } else if (info.getActiveStatement() instanceof Assignment) {
-                    Assignment assignment = (Assignment) info.getActiveStatement();
+                } else if (info.getActiveStatement() instanceof Assignment assignment) {
                     ExecutionContext context = extractContext(node, services);
                     LinkedHashSet<IProofReference<?>> result =
                         new LinkedHashSet<>();
@@ -110,7 +109,7 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
             IProgramMethod pm = mr.method(services, refPrefixType, context);
             return new DefaultProofReference<>(IProofReference.CALL_METHOD, node, pm);
         } else {
-            if (!(node.getAppliedRuleApp() instanceof PosTacletApp)) {
+            if (!(node.getAppliedRuleApp() instanceof PosTacletApp app)) {
                 throw new IllegalArgumentException("PosTacletApp expected.");
             }
             if (!"staticMethodCallStaticWithAssignmentViaTypereference"
@@ -119,7 +118,6 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
                     "Rule \"staticMethodCallStaticWithAssignmentViaTypereference\" expected, but is \""
                         + MiscTools.getRuleName(node) + "\".");
             }
-            PosTacletApp app = (PosTacletApp) node.getAppliedRuleApp();
             SchemaVariable methodSV = app.instantiations().lookupVar(new Name("#mn"));
             SchemaVariable typeSV = app.instantiations().lookupVar(new Name("#t"));
             SchemaVariable argsSV = app.instantiations().lookupVar(new Name("#elist"));

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java

@@ -70,8 +70,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
                         (ProgramVariable) pe);
                 ProofReferenceUtil.merge(toFill, reference);
             }
-        } else if (pe instanceof FieldReference) {
-            FieldReference fr = (FieldReference) pe;
+        } else if (pe instanceof FieldReference fr) {
             ReferencePrefix ref = fr.getReferencePrefix();
             if (ref != null) {
                 listReferences(node, ref, arrayLength, toFill, includeExpressionContainer);
@@ -82,8 +81,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
                     new DefaultProofReference<>(IProofReference.ACCESS, node, pv);
                 ProofReferenceUtil.merge(toFill, reference);
             }
-        } else if (includeExpressionContainer && pe instanceof ExpressionContainer) {
-            ExpressionContainer ec = (ExpressionContainer) pe;
+        } else if (includeExpressionContainer && pe instanceof ExpressionContainer ec) {
             for (int i = ec.getChildCount() - 1; i >= 0; i--) {
                 ProgramElement element = ec.getChildAt(i);
                 listReferences(node, element, arrayLength, toFill, includeExpressionContainer);

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java

@@ -95,8 +95,7 @@ public Proof getSource() {
      */
     @Override
     public boolean equals(Object obj) {
-        if (obj instanceof IProofReference<?>) {
-            IProofReference<?> other = (IProofReference<?>) obj;
+        if (obj instanceof IProofReference<?> other) {
             return Objects.equals(getKind(), other.getKind())
                     && Objects.equals(getSource(), other.getSource())
                     && Objects.equals(getTarget(), other.getTarget());

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/IProofReference.java

@@ -23,7 +23,7 @@
  *
  * @author Martin Hentschel
  * @see ProofReferenceUtil
- * @see IProofReferencesAnalyst.
+ * @see IProofReferencesAnalyst
  */
 public interface IProofReference<T> {
     /**

key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java

@@ -235,10 +235,10 @@ protected void assertReferences(LinkedHashSet<IProofReference<?>> current,
         int i = 0;
         for (IProofReference<?> currentReference : current) {
             ExpectedProofReferences expectedReference = expected[i];
-            assertEquals(expectedReference.getKind(), currentReference.getKind());
-            if (expectedReference.getTarget() != null) {
+            assertEquals(expectedReference.kind(), currentReference.getKind());
+            if (expectedReference.target() != null) {
                 assertNotNull(currentReference.getTarget());
-                assertEquals(expectedReference.getTarget(),
+                assertEquals(expectedReference.target(),
                     currentReference.getTarget().toString());
             } else {
                 assertNull(currentReference.getTarget());
@@ -250,48 +250,40 @@ protected void assertReferences(LinkedHashSet<IProofReference<?>> current,
     /**
      * Defines the values of an expected proof reference.
      *
+     * @param kind   The expected kind.
+     * @param target The expected target.
      * @author Martin Hentschel
      */
-    protected static class ExpectedProofReferences {
-        /**
-         * The expected kind.
-         */
-        private final String kind;
-
-        /**
-         * The expected target.
-         */
-        private final String target;
-
+        protected record ExpectedProofReferences(String kind, String target) {
         /**
          * Constructor.
          *
-         * @param kind The expected kind.
+         * @param kind   The expected kind.
          * @param target The expected target.
          */
-        public ExpectedProofReferences(String kind, String target) {
-            this.kind = kind;
-            this.target = target;
+        public ExpectedProofReferences {
         }
 
-        /**
-         * Returns the expected kind.
-         *
-         * @return The expected kind.
-         */
-        public String getKind() {
-            return kind;
-        }
+            /**
+             * Returns the expected kind.
+             *
+             * @return The expected kind.
+             */
+            @Override
+            public String kind() {
+                return kind;
+            }
 
-        /**
-         * Returns the expected target.
-         *
-         * @return The expected target.
-         */
-        public String getTarget() {
-            return target;
+            /**
+             * Returns the expected target.
+             *
+             * @return The expected target.
+             */
+            @Override
+            public String target() {
+                return target;
+            }
         }
-    }
 
     /**
      * Does some test steps with a {@link Proof}.

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java

@@ -34,9 +34,7 @@ public void visit(Term t) {
 
     private void addVarsToKeep() {
         for (IBreakpoint breakpoint : breakpointStopCondition.getBreakpoints()) {
-            if (breakpoint instanceof AbstractConditionalBreakpoint) {
-                AbstractConditionalBreakpoint conditionalBreakpoint =
-                    (AbstractConditionalBreakpoint) breakpoint;
+            if (breakpoint instanceof AbstractConditionalBreakpoint conditionalBreakpoint) {
                 if (conditionalBreakpoint.getToKeep() != null) {
                     for (LocationVariable sub : conditionalBreakpoint.getToKeep()) {
                         if (sub instanceof LocationVariable) {