polish

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

@@ -21,13 +21,13 @@
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.Pair;

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

@@ -22,13 +22,13 @@
 import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
 import de.uka.ilkd.key.rule.QueryExpand;
-import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.logic.Name;
 import org.key_project.logic.sort.Sort;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 
 import org.jspecify.annotations.NonNull;

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

@@ -608,10 +608,10 @@ public ImmutableList<Goal> apply(final RuleApp ruleApp) {
          * caught.
          */
         NamespaceSet originalNamespaces = getLocalNamespaces();
-        Services overlayServices = proof.getServices().getOverlay(originalNamespaces);
         final ImmutableList<Goal> goalList;
         var time = System.nanoTime();
         try {
+            Services overlayServices = proof.getServices().getOverlay(originalNamespaces);
             goalList = ruleApp.execute(this, overlayServices);
         } finally {
             PERF_APP_EXECUTE.getAndAdd(System.nanoTime() - time);

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

@@ -515,8 +515,7 @@ private ImmutableList<Goal> filterEnabledGoals(ImmutableList<Goal> goals) {
      *
      * @param oldGoal the old goal that has to be removed from list
      * @param newGoals the Iterable<Goal> with the new goals that were result of a rule application
-     *        on
-     *        goal
+     *        on goal
      */
     @Override
     public void replace(Goal oldGoal, Iterable<Goal> newGoals) {

key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java

@@ -7,7 +7,6 @@
 import de.uka.ilkd.key.proof.Goal;
 
 import org.key_project.logic.HasOrigin;
-import org.key_project.logic.Name;
 import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 
@@ -32,18 +31,9 @@ public interface Rule extends org.key_project.ncore.rules.Rule, HasOrigin {
     ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             throws RuleAbortException;
 
+
     @NonNull
     default ImmutableList<Goal> apply(Goal goal, RuleApp ruleApp) throws RuleAbortException {
-      return apply(goal, goal.proof().getServices(), ruleApp);
+        return apply(goal, goal.proof().getServices(), ruleApp);
     };
-
-    /**
-     * the name of the rule
-     */
-    Name name();
-
-    /**
-     * returns the display name of the rule
-     */
-    String displayName();
 }

key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java

@@ -28,13 +28,13 @@
 import de.uka.ilkd.key.proof.ProofTreeEvent;
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.util.mergerule.SymbolicExecutionState;
 
 import org.key_project.logic.Name;
 import org.key_project.logic.op.Function;
 import org.key_project.logic.sort.Sort;
+import org.key_project.ncore.rules.RuleAbortException;
 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/rule/merge/MergeRule.java

@@ -24,7 +24,6 @@
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
 import de.uka.ilkd.key.rule.NoPosTacletApp;
-import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.merge.MergeProcedure.ValuesMergeResult;
 import de.uka.ilkd.key.rule.merge.procedures.MergeByIfThenElse;
@@ -40,6 +39,7 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.op.Function;
 import org.key_project.logic.sort.Sort;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;

key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java

@@ -19,7 +19,6 @@
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.rule.Rule;
-import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy;
 import de.uka.ilkd.key.rule.label.TermLabelPolicy;
@@ -29,6 +28,7 @@
 import de.uka.ilkd.key.util.HelperClassForTests;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;

key.ncore.calculus/src/main/java/org/key_project/ncore/rules/Rule.java

@@ -1,11 +1,15 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.ncore.rules;
 
-import org.jspecify.annotations.NonNull;
 import org.key_project.logic.Name;
 import org.key_project.logic.Named;
 import org.key_project.ncore.proof.ProofGoal;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.NonNull;
+
 public interface Rule extends Named {
     /**
      * the rule is applied on the given goal using the information of rule application.
@@ -28,5 +32,7 @@ <G extends ProofGoal> ImmutableList<G> apply(G goal, RuleApp ruleApp)
     /**
      * returns the display name of the rule
      */
-    String displayName();
+    default String displayName() {
+        return name().toString();
+    }
 }

key.ncore.calculus/src/main/java/org/key_project/ncore/rules/RuleAbortException.java

@@ -10,9 +10,7 @@
  *         This Exception signals the abort of a rule Application
  *
  */
-
-
-public class RuleAbortException extends Exception {
+public class RuleAbortException extends RuntimeException {
 
     private static final long serialVersionUID = -645034125571021135L;
 

key.ncore.calculus/src/main/java/org/key_project/ncore/rules/RuleApp.java

@@ -1,9 +1,13 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.ncore.rules;
 
-import org.jspecify.annotations.Nullable;
 import org.key_project.ncore.proof.ProofGoal;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.Nullable;
+
 public interface RuleApp {
     /**
      * returns the rule of this rule application

key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java

@@ -26,11 +26,11 @@
 import de.uka.ilkd.key.pp.AbbrevMap;
 import de.uka.ilkd.key.pp.PrettyPrinter;
 import de.uka.ilkd.key.proof.io.OutputStreamProofSaver;
-import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.speclang.LoopSpecification;
 import de.uka.ilkd.key.util.InfFlowSpec;
 
 import org.key_project.logic.sort.Sort;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 

key.ui/src/main/java/de/uka/ilkd/key/gui/LoopInvariantRuleCompletion.java

@@ -13,6 +13,7 @@
 import de.uka.ilkd.key.speclang.LoopSpecImpl;
 import de.uka.ilkd.key.speclang.LoopSpecification;
 import de.uka.ilkd.key.util.MiscTools;
+
 import org.key_project.ncore.rules.RuleAbortException;
 
 /**