Code cleanup (#3064)

This MR does some automated code cleanup.
Lots of changes, I grouped the changes in commits and the review should
happen on a per commit basis.

Some of them might be debateable, please do so.
However, I think most of them really help with parsing of and reasoning
about the code.

- [x] Blocking on #3026.

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java

@@ -114,7 +114,7 @@ private static class ReferenceAnalaystProofVisitor implements ProofVisitor {
          * The result.
          */
         private final LinkedHashSet<IProofReference<?>> result =
-            new LinkedHashSet<IProofReference<?>>();
+            new LinkedHashSet<>();
 
         /**
          * Constructor.
@@ -168,7 +168,7 @@ public static LinkedHashSet<IProofReference<?>> computeProofReferences(Node node
      */
     public static LinkedHashSet<IProofReference<?>> computeProofReferences(Node node,
             Services services, ImmutableList<IProofReferencesAnalyst> analysts) {
-        LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+        LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
         if (node != null && analysts != null) {
             for (IProofReferencesAnalyst analyst : analysts) {
                 LinkedHashSet<IProofReference<?>> analystResult =

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

@@ -66,19 +66,19 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                     // Invariant was applied
                     PartialInvAxiom axiom = (PartialInvAxiom) found;
                     DefaultProofReference<ClassInvariant> reference =
-                        new DefaultProofReference<ClassInvariant>(IProofReference.USE_INVARIANT,
+                        new DefaultProofReference<>(IProofReference.USE_INVARIANT,
                             node, axiom.getInv());
                     LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<IProofReference<?>>();
+                        new LinkedHashSet<>();
                     result.add(reference);
                     return result;
                 } else if (found != null) {
                     // ClassAxiom was applied
                     DefaultProofReference<ClassAxiom> reference =
-                        new DefaultProofReference<ClassAxiom>(IProofReference.USE_AXIOM, node,
+                        new DefaultProofReference<>(IProofReference.USE_AXIOM, node,
                             found);
                     LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<IProofReference<?>>();
+                        new LinkedHashSet<>();
                     result.add(reference);
                     return result;
                 } else {

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

@@ -23,9 +23,9 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
         if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp) {
             AbstractContractRuleApp contractRuleApp =
                 (AbstractContractRuleApp) node.getAppliedRuleApp();
-            DefaultProofReference<Contract> reference = new DefaultProofReference<Contract>(
+            DefaultProofReference<Contract> reference = new DefaultProofReference<>(
                 IProofReference.USE_CONTRACT, node, contractRuleApp.getInstantiation());
-            LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+            LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
             result.add(reference);
             return result;
         } else {

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

@@ -31,5 +31,5 @@ public interface IProofReferencesAnalyst {
      * @return The found {@link IProofReference} or {@code null}/empty set if the applied rule is
      *         not supported.
      */
-    public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services);
+    LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services);
 }

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

@@ -27,9 +27,9 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                 MethodBodyStatement mbs = (MethodBodyStatement) info.getActiveStatement();
                 IProgramMethod pm = mbs.getProgramMethod(services);
                 DefaultProofReference<IProgramMethod> reference =
-                    new DefaultProofReference<IProgramMethod>(IProofReference.INLINE_METHOD, node,
+                    new DefaultProofReference<>(IProofReference.INLINE_METHOD, node,
                         pm);
-                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
                 result.add(reference);
                 return result;
             } else {

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

@@ -6,7 +6,6 @@
 import de.uka.ilkd.key.java.ProgramElement;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.abstraction.Type;
 import de.uka.ilkd.key.java.expression.Assignment;
 import de.uka.ilkd.key.java.reference.ExecutionContext;
 import de.uka.ilkd.key.java.reference.MethodReference;
@@ -50,14 +49,14 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                     IProofReference<IProgramMethod> reference = createReference(node, services,
                         context, (MethodReference) info.getActiveStatement());
                     LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<IProofReference<?>>();
+                        new LinkedHashSet<>();
                     result.add(reference);
                     return result;
                 } else if (info.getActiveStatement() instanceof Assignment) {
                     Assignment assignment = (Assignment) info.getActiveStatement();
                     ExecutionContext context = extractContext(node, services);
                     LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<IProofReference<?>>();
+                        new LinkedHashSet<>();
                     for (int i = 0; i < assignment.getChildCount(); i++) {
                         ProgramElement child = assignment.getChildAt(i);
                         if (child instanceof MethodReference) {
@@ -106,7 +105,7 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
         if (context != null) {
             KeYJavaType refPrefixType = mr.determineStaticPrefixType(services, context);
             IProgramMethod pm = mr.method(services, refPrefixType, context);
-            return new DefaultProofReference<IProgramMethod>(IProofReference.CALL_METHOD, node, pm);
+            return new DefaultProofReference<>(IProofReference.CALL_METHOD, node, pm);
         } else {
             if (!(node.getAppliedRuleApp() instanceof PosTacletApp)) {
                 throw new IllegalArgumentException("PosTacletApp expected.");
@@ -131,8 +130,8 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
                 throw new IllegalArgumentException("Empty argument list expected.");
             }
             IProgramMethod pm = services.getJavaInfo().getProgramMethod(type.getKeYJavaType(),
-                method.toString(), ImmutableSLList.<Type>nil(), type.getKeYJavaType());
-            return new DefaultProofReference<IProgramMethod>(IProofReference.CALL_METHOD, node, pm);
+                method.toString(), ImmutableSLList.nil(), type.getKeYJavaType());
+            return new DefaultProofReference<>(IProofReference.CALL_METHOD, node, pm);
         }
     }
 }

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

@@ -31,12 +31,12 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
         if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
             SourceElement statement = node.getNodeInfo().getActiveStatement();
             if (statement instanceof CopyAssignment) {
-                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
                 listReferences(node, (CopyAssignment) statement,
                     services.getJavaInfo().getArrayLength(), result, true);
                 return result;
             } else if (statement instanceof If) {
-                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
                 listReferences(node, ((If) statement).getExpression(),
                     services.getJavaInfo().getArrayLength(), result, false);
                 return result;
@@ -63,7 +63,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
             ProgramVariable pv = (ProgramVariable) pe;
             if (pv.isMember()) {
                 DefaultProofReference<ProgramVariable> reference =
-                    new DefaultProofReference<ProgramVariable>(IProofReference.ACCESS, node,
+                    new DefaultProofReference<>(IProofReference.ACCESS, node,
                         (ProgramVariable) pe);
                 ProofReferenceUtil.merge(toFill, reference);
             }
@@ -76,7 +76,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
             ProgramVariable pv = fr.getProgramVariable();
             if (pv != arrayLength) {
                 DefaultProofReference<ProgramVariable> reference =
-                    new DefaultProofReference<ProgramVariable>(IProofReference.ACCESS, node, pv);
+                    new DefaultProofReference<>(IProofReference.ACCESS, node, pv);
                 ProofReferenceUtil.merge(toFill, reference);
             }
         } else if (includeExpressionContainer && pe instanceof ExpressionContainer) {

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

@@ -16,22 +16,22 @@ public class DefaultProofReference<T> implements IProofReference<T> {
     /**
      * The reference kind as human readable {@link String}.
      */
-    private String kind;
+    private final String kind;
 
     /**
      * The source {@link Proof}.
      */
-    private Proof source;
+    private final Proof source;
 
     /**
      * The target source member.
      */
-    private T target;
+    private final T target;
 
     /**
      * The {@link Node} in which the reference was found.
      */
-    private LinkedHashSet<Node> nodes = new LinkedHashSet<Node>();
+    private final LinkedHashSet<Node> nodes = new LinkedHashSet<>();
 
     /**
      * Constructor

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

@@ -32,7 +32,7 @@ public interface IProofReference<T> {
      * ({@link #getTarget()}).
      * </p>
      */
-    public static final String CALL_METHOD = "Call Method";
+    String CALL_METHOD = "Call Method";
 
     /**
      * <p>
@@ -43,7 +43,7 @@ public interface IProofReference<T> {
      * ({@link #getTarget()}).
      * </p>
      */
-    public static final String INLINE_METHOD = "Inline Method";
+    String INLINE_METHOD = "Inline Method";
 
     /**
      * <p>
@@ -54,7 +54,7 @@ public interface IProofReference<T> {
      * References of this kind should provide a {@link Contract} as target ({@link #getTarget()}).
      * </p>
      */
-    public static final String USE_CONTRACT = "Use Contract";
+    String USE_CONTRACT = "Use Contract";
 
     /**
      * <p>
@@ -65,7 +65,7 @@ public interface IProofReference<T> {
      * ({@link #getTarget()}).
      * </p>
      */
-    public static final String ACCESS = "Access";
+    String ACCESS = "Access";
 
     /**
      * <p>
@@ -76,7 +76,7 @@ public interface IProofReference<T> {
      * ({@link #getTarget()}).
      * </p>
      */
-    public static final String USE_INVARIANT = "Use Invariant";
+    String USE_INVARIANT = "Use Invariant";
 
     /**
      * <p>
@@ -87,40 +87,40 @@ public interface IProofReference<T> {
      * ({@link #getTarget()}).
      * </p>
      */
-    public static final String USE_AXIOM = "Use Axiom";
+    String USE_AXIOM = "Use Axiom";
 
     /**
      * Returns the reference kind which is a human readable {@link String}.
      *
      * @return The reference kind as human readable {@link String}.
      */
-    public String getKind();
+    String getKind();
 
     /**
      * Returns the {@link Node}s in which the reference was found.
      *
      * @return The {@link Node}s in which the reference was found.
      */
-    public LinkedHashSet<Node> getNodes();
+    LinkedHashSet<Node> getNodes();
 
     /**
      * Adds the given {@link Node}s to the own {@link Node}s.
      *
      * @param nodes The {@link Node}s to add.
      */
-    public void addNodes(Collection<Node> nodes);
+    void addNodes(Collection<Node> nodes);
 
     /**
      * Returns the target source member.
      *
      * @return The target source member.
      */
-    public T getTarget();
+    T getTarget();
 
     /**
      * Returns the source {@link Proof}.
      *
      * @return The source {@link Proof}.
      */
-    public Proof getSource();
+    Proof getSource();
 }

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

@@ -156,7 +156,7 @@ protected IProofTester createReferenceMethodTester(final IProofReferencesAnalyst
             // Filter references
             if (currentReferenceFilter != null) {
                 LinkedHashSet<IProofReference<?>> filteredReferences =
-                    new LinkedHashSet<IProofReference<?>>();
+                    new LinkedHashSet<>();
                 for (IProofReference<?> reference : references) {
                     if (currentReferenceFilter.test(reference)) {
                         filteredReferences.add(reference);
@@ -179,7 +179,7 @@ protected IProofTester createReferenceMethodTester(final IProofReferencesAnalyst
      */
     protected LinkedHashSet<IProofReference<?>> findReferences(
             LinkedHashSet<IProofReference<?>> references, Node node) {
-        LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+        LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
         for (IProofReference<?> reference : references) {
             if (reference.getNodes().contains(node)) {
                 result.add(reference);

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

@@ -4,14 +4,13 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.logic.op.Modality;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
 import de.uka.ilkd.key.strategy.IBreakpointStopCondition;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractConditionalBreakpoint;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
 
 public class TermProgramVariableCollectorKeepUpdatesForBreakpointconditions
         extends TermProgramVariableCollector {
-    private IBreakpointStopCondition breakpointStopCondition;
+    private final IBreakpointStopCondition breakpointStopCondition;
 
     public TermProgramVariableCollectorKeepUpdatesForBreakpointconditions(Services services,
             IBreakpointStopCondition breakpointStopCondition) {
@@ -36,9 +35,9 @@ private void addVarsToKeep() {
                 AbstractConditionalBreakpoint conditionalBreakpoint =
                     (AbstractConditionalBreakpoint) breakpoint;
                 if (conditionalBreakpoint.getToKeep() != null) {
-                    for (SVSubstitute sub : conditionalBreakpoint.getToKeep()) {
+                    for (LocationVariable sub : conditionalBreakpoint.getToKeep()) {
                         if (sub instanceof LocationVariable) {
-                            super.result().add((LocationVariable) sub);
+                            super.result().add(sub);
                         }
                     }
                 }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java

@@ -35,10 +35,9 @@ public boolean mergeLabels(SequentFormula existingSF, Term existingTerm,
             mergedLabels.remove(existingLabel);
             // Add new label
             mergedLabels.add(newLabel);
-            return true;
         } else {
             mergedLabels.add(rejectedLabel);
-            return true;
         }
+        return true;
     }
 }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java

@@ -248,7 +248,7 @@ protected void refactorSequentFormulas(TermLabelState state, Services services,
             FormulaTermLabel termLabel = (FormulaTermLabel) term.getLabel(FormulaTermLabel.NAME);
             if (termLabel != null) {
                 labels.remove(termLabel);
-                Set<String> beforeIds = new LinkedHashSet<String>();
+                Set<String> beforeIds = new LinkedHashSet<>();
                 beforeIds.add(termLabel.getId());
                 int labelSubID = FormulaTermLabel.newLabelSubID(services, termLabel);
                 labels.add(new FormulaTermLabel(termLabel.getMajorId(), labelSubID, beforeIds));
@@ -318,7 +318,7 @@ public static void setInnerMostParentRefactored(TermLabelState state, Goal goal,
             boolean refactored) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         labelState.put(INNER_MOST_PARENT_REFACTORED_PREFIX + goal.node().serialNr(),
-            Boolean.valueOf(refactored));
+            refactored);
     }
 
     /**
@@ -330,7 +330,7 @@ public static void setInnerMostParentRefactored(TermLabelState state, Goal goal,
     public static boolean isUpdateRefactroingRequired(TermLabelState state) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         Object value = labelState.get(UPDATE_REFACTORING_REQUIRED);
-        return value instanceof Boolean && ((Boolean) value).booleanValue();
+        return value instanceof Boolean && (Boolean) value;
     }
 
     /**
@@ -341,7 +341,7 @@ public static boolean isUpdateRefactroingRequired(TermLabelState state) {
      */
     public static void setUpdateRefactroingRequired(TermLabelState state, boolean required) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
-        labelState.put(UPDATE_REFACTORING_REQUIRED, Boolean.valueOf(required));
+        labelState.put(UPDATE_REFACTORING_REQUIRED, required);
     }
 
     /**
@@ -353,7 +353,7 @@ public static void setUpdateRefactroingRequired(TermLabelState state, boolean re
     public static boolean isParentRefactroingRequired(TermLabelState state) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         Object value = labelState.get(PARENT_REFACTORING_REQUIRED);
-        return value instanceof Boolean && ((Boolean) value).booleanValue();
+        return value instanceof Boolean && (Boolean) value;
     }
 
     /**
@@ -364,7 +364,7 @@ public static boolean isParentRefactroingRequired(TermLabelState state) {
      */
     public static void setParentRefactroingRequired(TermLabelState state, boolean required) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
-        labelState.put(PARENT_REFACTORING_REQUIRED, Boolean.valueOf(required));
+        labelState.put(PARENT_REFACTORING_REQUIRED, required);
     }
 
     /**

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java

@@ -76,7 +76,7 @@ public void updateLabels(TermLabelState state, Services services,
             TacletApp ta = (TacletApp) ruleApp;
             if (ta.ifInstsComplete() && ta.ifFormulaInstantiations() != null) {
                 Map<SequentFormula, FormulaTermLabel> ifLabels =
-                    new LinkedHashMap<SequentFormula, FormulaTermLabel>();
+                    new LinkedHashMap<>();
                 for (IfFormulaInstantiation ifInst : ta.ifFormulaInstantiations()) {
                     FormulaTermLabel ifLabel = StayOnFormulaTermLabelPolicy.searchFormulaTermLabel(
                         ifInst.getConstrainedFormula().formula().getLabels());