Some general minor code quality improvements

key.core/src/main/java/de/uka/ilkd/key/proof/InstantiationProposerCollection.java

@@ -29,8 +29,7 @@ public void add(InstantiationProposer proposer) {
 
     public String getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor,
             ImmutableList<String> previousProposals) {
-        for (InstantiationProposer proposer1 : proposers) {
-            InstantiationProposer proposer = proposer1;
+        for (InstantiationProposer proposer : proposers) {
             String proposal =
                 proposer.getProposal(app, var, services, undoAnchor, previousProposals);
             if (proposal != null) {

key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java

@@ -19,7 +19,6 @@
 import de.uka.ilkd.key.rule.NoPosTacletApp;
 import de.uka.ilkd.key.rule.inst.*;
 
-import org.key_project.util.collection.*;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java

@@ -4,7 +4,6 @@
 package de.uka.ilkd.key.proof;
 
 
-import java.net.MalformedURLException;
 import javax.annotation.Nullable;
 
 import de.uka.ilkd.key.java.Position;
@@ -61,7 +60,7 @@ public String toString() {
 
     @Nullable
     @Override
-    public Location getLocation() throws MalformedURLException {
+    public Location getLocation() {
         return new Location(null, position);
     }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java

@@ -58,7 +58,7 @@ public class TacletAppIndex {
      */
     private RuleFilter ruleFilter;
 
-    private State state;
+    private final State state;
 
     private final Map<CacheKey, TermTacletAppIndex> cache;
 

key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java

@@ -379,7 +379,7 @@ private ImmutableList<NoPosTacletApp> getListHelp(
      * @param second the second list
      * @return the merged list
      */
-    private final ImmutableList<NoPosTacletApp> merge(ImmutableList<NoPosTacletApp> first,
+    private ImmutableList<NoPosTacletApp> merge(ImmutableList<NoPosTacletApp> first,
             final ImmutableList<NoPosTacletApp> second) {
         if (second == null) {
             return first;
@@ -579,9 +579,7 @@ private static class PrefixOccurrences {
          * resets the occurred field to 'nothing has occurred'
          */
         public void reset() {
-            for (int i = 0; i < PREFIXTYPES; i++) {
-                occurred[i] = false;
-            }
+            Arrays.fill(occurred, 0, PREFIXTYPES, false);
         }
 
         /**

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

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.init;
 
-import java.io.IOException;
 import java.util.*;
 
 import de.uka.ilkd.key.java.Services;
@@ -302,10 +301,8 @@ public void fillSaveProperties(Properties properties) {
      * @param initConfig The already load {@link InitConfig}.
      * @param properties The settings of the proof obligation to instantiate.
      * @return The instantiated proof obligation.
-     * @throws IOException Occurred Exception.
      */
-    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
-            throws IOException {
+    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
         String contractName = properties.getProperty("contract");
         int proofNum = 0;
         String baseContractName = null;

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

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.init;
 
-import java.io.IOException;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
@@ -80,10 +79,8 @@ public FunctionalBlockContractPO(InitConfig initConfig, FunctionalBlockContract
      * @param initConfig The already load {@link InitConfig}.
      * @param properties The settings of the proof obligation to instantiate.
      * @return The instantiated proof obligation.
-     * @throws IOException Occurred Exception.
      */
-    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
-            throws IOException {
+    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
         String contractName = properties.getProperty("contract");
         int proofNum = 0;
         String baseContractName = null;
@@ -339,7 +336,7 @@ public boolean equals(Object obj) {
     }
 
     @Override
-    public void readProblem() throws ProofInputException {
+    public void readProblem() {
         assert proofConfig == null;
         final boolean makeNamesUnique = true;
         final Services services = postInit();

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

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.init;
 
-import java.io.IOException;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
@@ -80,10 +79,8 @@ public FunctionalLoopContractPO(InitConfig initConfig, FunctionalLoopContract co
      * @param initConfig The already load {@link InitConfig}.
      * @param properties The settings of the proof obligation to instantiate.
      * @return The instantiated proof obligation.
-     * @throws IOException Occurred Exception.
      */
-    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
-            throws IOException {
+    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
         String contractName = properties.getProperty("contract");
         int proofNum = 0;
         String baseContractName = null;
@@ -161,7 +158,7 @@ public boolean equals(Object obj) {
     }
 
     @Override
-    public void readProblem() throws ProofInputException {
+    public void readProblem() {
         assert proofConfig == null;
         final boolean makeNamesUnique = true;
         final Services services = postInit();

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

@@ -62,7 +62,7 @@
  */
 public class FunctionalOperationContractPO extends AbstractOperationPO implements ContractPO {
     public static final Map<Boolean, String> TRANSACTION_TAGS =
-        new LinkedHashMap<Boolean, String>();
+        new LinkedHashMap<>();
 
     private final FunctionalOperationContract contract;
 
@@ -134,7 +134,7 @@ protected ImmutableList<StatementBlock> buildOperationBlocks(
             ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar,
             ProgramVariable resultVar, Services services) {
         final StatementBlock[] result = new StatementBlock[4];
-        final ImmutableArray<Expression> formalArray = new ImmutableArray<Expression>(
+        final ImmutableArray<Expression> formalArray = new ImmutableArray<>(
             formalParVars.toArray(new ProgramVariable[formalParVars.size()]));
 
         if (getContract().getTarget().isConstructor()) {

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

@@ -159,7 +159,7 @@ public String getProofObligation() {
     }
 
     @Override
-    public ProofAggregate getPO() throws ProofInputException {
+    public ProofAggregate getPO() {
         assert problem != null;
         String name = name();
         ProofSettings settings = getPreferences();
@@ -181,7 +181,7 @@ public boolean hasProofScript() {
         return getParseContext().findProofScript() != null;
     }
 
-    public Triple<String, Integer, Integer> readProofScript() throws ProofInputException {
+    public Triple<String, Integer, Integer> readProofScript() {
         return getParseContext().findProofScript();
     }
 
@@ -240,9 +240,8 @@ public Profile getProfile() {
      *
      * @return The {@link Profile} defined by the file to load or {@code null} if no {@link Profile}
      *         is defined by the file.
-     * @throws Exception Occurred Exception.
      */
-    private Profile readProfileFromFile() throws Exception {
+    private Profile readProfileFromFile() {
         @Nonnull
         ProblemInformation pi = getProblemInformation();
         String profileName = pi.getProfile();

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

@@ -239,11 +239,7 @@ private void readJava(EnvInput envInput, InitConfig initConfig) throws ProofInpu
         final String javaPath = envInput.readJavaPath();
         final List<File> classPath = envInput.readClassPath();
         final File bootClassPath;
-        try {
-            bootClassPath = envInput.readBootClassPath();
-        } catch (IOException ioe) {
-            throw new ProofInputException(ioe);
-        }
+        bootClassPath = envInput.readBootClassPath();
 
         final Includes includes = envInput.readIncludes();
 
@@ -384,8 +380,7 @@ private void populateNamespaces(Proof proof) {
     }
 
     // what is the purpose of this method?
-    private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig)
-            throws ProofInputException {
+    private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig) {
         // TODO: what does this actually do?
         ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().updateChoices(initConfig.choiceNS(),
             false);

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

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.init;
 
-import java.io.IOException;
 import java.util.LinkedHashMap;
 import java.util.Map;
 import java.util.Properties;
@@ -199,13 +198,12 @@ private void register(Variables vars, Services proofServices) {
     protected ImmutableSet<ClassAxiom> selectClassAxioms(KeYJavaType kjt) {
         ImmutableSet<ClassAxiom> result = DefaultImmutableSet.nil();
         for (ClassAxiom axiom : specRepos.getClassAxioms(kjt)) {
-            if (axiom instanceof ClassAxiom && check instanceof ClassWellDefinedness cwd) {
-                final ClassAxiom classAxiom = axiom;
+            if (check instanceof ClassWellDefinedness cwd) {
                 final String kjtName = cwd.getKJT().getFullName();
                 final String invName = "in " + cwd.getKJT().getName();
-                if (!classAxiom.getName().endsWith(invName)
-                        && !classAxiom.getName().endsWith(kjtName)) {
-                    result = result.add(classAxiom);
+                if (!axiom.getName().endsWith(invName)
+                        && !axiom.getName().endsWith(kjtName)) {
+                    result = result.add(axiom);
                 }
             } else {
                 result = result.add(axiom);
@@ -227,7 +225,7 @@ public KeYJavaType getKJT() {
     }
 
     @Override
-    public void readProblem() throws ProofInputException {
+    public void readProblem() {
         assert proofConfig == null;
 
         final Services proofServices = postInit();
@@ -300,10 +298,8 @@ public void fillSaveProperties(Properties properties) {
      * @param initConfig The already load {@link InitConfig}.
      * @param properties The settings of the proof obligation to instantiate.
      * @return The instantiated proof obligation.
-     * @throws IOException Occurred Exception.
      */
-    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
-            throws IOException {
+    public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
         String contractName = properties.getProperty("wd check");
         final Contract contract =
             initConfig.getServices().getSpecificationRepository().getContractByName(contractName);

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

@@ -4,7 +4,6 @@
 package de.uka.ilkd.key.proof.io;
 
 import java.io.File;
-import java.io.IOException;
 import java.util.List;
 import javax.annotation.Nonnull;
 import javax.annotation.Nullable;
@@ -59,7 +58,6 @@ public interface EnvInput {
         return null;
     }
 
-
     /**
      * gets the classpath elements to be considered here.
      */
@@ -68,10 +66,8 @@ public interface EnvInput {
 
     /**
      * gets the boot classpath element, null if none set.
-     *
-     * @throws
      */
-    File readBootClassPath() throws IOException;
+    File readBootClassPath();
 
     /**
      * Reads the input using the given modification strategy, i.e., parts of the input do not modify

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

@@ -45,7 +45,6 @@
 import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.smt.*;
-import de.uka.ilkd.key.smt.SMTRuleApp;
 import de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth;
 import de.uka.ilkd.key.speclang.Contract;
 import de.uka.ilkd.key.speclang.OperationContract;

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

@@ -39,7 +39,8 @@ public interface LDTInputListener {
      * creates a representation of the LDT files to be used as input to the KeY prover.
      *
      * @param keyFiles an array containing the LDT .key files
-     * @param main the main class used to report the progress of reading
+     * @param listener an LDTInputListener for stsus reports while loading
+     * @param profile the Profile for which the LDTs are load
      */
     public LDTInput(KeYFile[] keyFiles, LDTInputListener listener, Profile profile) {
         assert profile != null;
@@ -85,14 +86,14 @@ public Includes readIncludes() throws ProofInputException {
 
 
     @Override
-    public String readJavaPath() throws ProofInputException {
+    public String readJavaPath() {
         return "";
     }
 
 
     // no class path elements here
     @Override
-    public List<File> readClassPath() throws ProofInputException {
+    public List<File> readClassPath() {
         return null;
     }
 
@@ -111,7 +112,7 @@ public File readBootClassPath() {
      * declared sorts in all rules, e.g.
      */
     @Override
-    public ImmutableSet<PositionedString> read() throws ProofInputException {
+    public ImmutableSet<PositionedString> read() {
         if (initConfig == null) {
             throw new IllegalStateException("LDTInput: InitConfig not set.");
         }
@@ -162,7 +163,6 @@ public boolean equals(Object o) {
         return true;
     }
 
-
     @Override
     public int hashCode() {
         int result = 0;

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

@@ -87,7 +87,7 @@ protected void save(File file) throws IOException {
         save(new FileOutputStream(file));
     }
 
-    public String save() throws IOException {
+    public String save() {
         String errorMsg = null;
         try {
             save(file);

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

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.io.consistency;
 
-import java.io.IOException;
 import java.io.InputStream;
 import java.io.OutputStream;
 import java.net.URL;
@@ -19,19 +18,19 @@
 public class MemoryFileRepo extends AbstractFileRepo {
 
     @Override
-    public InputStream getInputStream(Path path) throws IOException {
+    public InputStream getInputStream(Path path) {
         // TODO Auto-generated method stub
         return null;
     }
 
     @Override
-    public InputStream getInputStream(RuleSource ruleSource) throws IOException {
+    public InputStream getInputStream(RuleSource ruleSource) {
         // TODO Auto-generated method stub
         return null;
     }
 
     @Override
-    public InputStream getInputStream(URL url) throws IOException {
+    public InputStream getInputStream(URL url) {
         // TODO Auto-generated method stub
         return null;
     }