Provide additional String formating utility method to reduce code duplication

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

@@ -10,6 +10,8 @@
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 
+import org.key_project.util.Strings;
+
 /**
  * Default implementation of {@link IProofReference}.
  *
@@ -40,7 +42,7 @@ public class DefaultProofReference<T> implements IProofReference<T> {
      * Constructor
      *
      * @param kind The reference kind as human readable {@link String}.
-     * @param source The source {@link Proof}.
+     * @param node Node to access the source {@link Proof} (or null).
      * @param target The target source member.
      */
     public DefaultProofReference(String kind, Node node, T target) {
@@ -128,15 +130,7 @@ public String toString() {
         sb.append("\"");
         if (!getNodes().isEmpty()) {
             sb.append(" at node(s) ");
-            boolean afterFirst = false;
-            for (Node node : getNodes()) {
-                if (afterFirst) {
-                    sb.append(", ");
-                } else {
-                    afterFirst = true;
-                }
-                sb.append(node.serialNr());
-            }
+            sb.append(Strings.formatAsList(getNodes(), "", ", ", "", Node::serialNr));
         }
         if (getSource() != null) {
             sb.append(" of proof \"");

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java

@@ -26,7 +26,8 @@
 import recoder.java.JavaProgramFactory;
 import recoder.java.declaration.ClassDeclaration;
 import recoder.java.declaration.MethodDeclaration;
-import recoder.java.declaration.ParameterDeclaration;
+
+import static org.key_project.util.Strings.*;
 
 /**
  * Facet class for interpreting RIFL specifications. The Requirements for Information Flow Language
@@ -194,16 +195,8 @@
 
             ClassDeclaration clazz = (ClassDeclaration) cu.getPrimaryTypeDeclaration();
             for (MethodDeclaration mdecl : si.getSpecifiedMethodDeclarations()) {
-
-
-                StringBuilder sb = new StringBuilder();
-                for (ParameterDeclaration p : mdecl.getParameters()) {
-                    sb.append(p.getTypeReference().getName());
-                    sb.append(",");
-                }
-                if (sb.length() > 0) {
-                    sb.deleteCharAt(sb.length() - 1);
-                }
+                final StringBuilder sb = new StringBuilder();
+                sb.append(formatAsList(mdecl.getParameters(), "", ",", ""));
 
                 String poname = clazz.getFullName() + "[" + clazz.getFullName() + "\\\\:\\\\:"
                     + mdecl.getName() + "(" + sb + ")" + "]" + ".Non-interference contract.0";

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java

@@ -25,6 +25,7 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import org.key_project.util.Strings;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.ImmutableSet;
@@ -1500,18 +1501,11 @@
          */
         @Override
         public String toString() {
-            StringBuilder sb = new StringBuilder();
+            final StringBuilder sb = new StringBuilder();
             sb.append(currentNode.serialNr());
             sb.append(" starting from goals ");
-            boolean afterFirst = false;
-            for (Goal goal : startingGoals) {
-                if (afterFirst) {
-                    sb.append(", ");
-                } else {
-                    afterFirst = true;
-                }
-                sb.append(goal.node().serialNr());
-            }
+            sb.append(Strings.formatAsList(startingGoals, "", ", ", "",
+                ((java.util.function.Function<Goal, Node>) Goal::node).andThen(Node::serialNr)));
             return sb.toString();
         }
     }

key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java

@@ -20,6 +20,7 @@
 
 import org.key_project.util.EqualsModProofIrrelevancy;
 import org.key_project.util.EqualsModProofIrrelevancyUtil;
+import org.key_project.util.Strings;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
@@ -80,7 +81,7 @@ private enum ThreeValuedTruth {
     private int hashcode2 = -1;
 
     /**
-     * This flag indicates that the {@link Term} itself or one of its children contains a non empty
+     * This flag indicates that the {@link Term} itself or one of its children contains a non-empty
      * {@link JavaBlock}. {@link Term}s which provides a {@link JavaBlock} directly or indirectly
      * can't be cached because it is possible that the contained meta information inside the
      * {@link JavaBlock}, e.g. {@link PositionInfo}s, are different.
@@ -107,7 +108,7 @@ public TermImpl(Operator op, ImmutableArray<Term> subs,
         assert op != null;
         assert subs != null;
         this.op = op;
-        this.subs = subs.size() == 0 ? EMPTY_TERM_LIST : subs;
+        this.subs = subs.isEmpty() ? EMPTY_TERM_LIST : subs;
         this.boundVars = boundVars == null ? EMPTY_VAR_LIST : boundVars;
         this.javaBlock = javaBlock == null ? JavaBlock.EMPTY_JAVABLOCK : javaBlock;
         this.origin = origin;
@@ -120,7 +121,7 @@ public TermImpl(Operator op, ImmutableArray<Term> subs,
 
     /**
      * For which feature is this information needed?
-     * What is the fifference from {@link de.uka.ilkd.key.logic.label.OriginTermLabel}?
+     * What is the difference from {@link de.uka.ilkd.key.logic.label.OriginTermLabel}?
      */
     private final String origin;
 
@@ -158,7 +159,7 @@ private ImmutableSet<QuantifiableVariable> determineFreeVars() {
 
     /**
      * Checks whether the Term is valid on the top level. If this is the case this method returns
-     * the Term unmodified. Otherwise a TermCreationException is thrown.
+     * the Term unmodified. Otherwise, a TermCreationException is thrown.
      */
     public Term checked() {
         op.validTopLevelException(this);
@@ -653,26 +654,12 @@ public String toString() {
         } else {
             sb.append(op().name().toString());
             if (!boundVars.isEmpty()) {
-                sb.append("{");
-                for (int i = 0, n = boundVars.size(); i < n; i++) {
-                    sb.append(boundVars.get(i));
-                    if (i < n - 1) {
-                        sb.append(", ");
-                    }
-                }
-                sb.append("}");
+                sb.append(Strings.formatAsList(boundVars(), "{", ",", "}"));
             }
             if (arity() == 0) {
                 return sb.toString();
             }
-            sb.append("(");
-            for (int i = 0, ar = arity(); i < ar; i++) {
-                sb.append(sub(i));
-                if (i < ar - 1) {
-                    sb.append(",");
-                }
-            }
-            sb.append(")");
+            sb.append(Strings.formatAsList(subs(), "(", ",", ")"));
         }
 
         return sb.toString();

key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java

@@ -7,6 +7,7 @@
 import de.uka.ilkd.key.logic.sort.NullSort;
 import de.uka.ilkd.key.logic.sort.Sort;
 
+import org.key_project.util.Strings;
 import org.key_project.util.collection.ImmutableArray;
 
 
@@ -115,16 +116,7 @@ public final String proofToString() {
             new StringBuilder((sort() == Sort.FORMULA ? "" : sort().toString()) + " ");
         s.append(name());
         if (arity() > 0) {
-            int i = 0;
-            s.append("(");
-            while (i < arity()) {
-                if (i > 0) {
-                    s.append(",");
-                }
-                s.append(argSort(i));
-                i++;
-            }
-            s.append(")");
+            s.append(Strings.formatAsList(argSorts(), "(", ",", ")"));
         }
         s.append(";\n");
         return s.toString();

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

@@ -29,6 +29,8 @@
 import org.key_project.util.collection.ImmutableMap;
 import org.key_project.util.collection.ImmutableSet;
 
+import static org.key_project.util.Strings.formatAsList;
+
 
 /**
  * Taclets are the DL-extension of schematic theory specific rules. They are used to describe rules
@@ -586,7 +588,6 @@ StringBuffer toStringIf(StringBuffer sb) {
     }
 
     StringBuffer toStringVarCond(StringBuffer sb) {
-
         if (!varsNew.isEmpty() || !varsNotFreeIn.isEmpty() || !variableConditions.isEmpty()) {
             sb = sb.append("\\varcond(");
 
@@ -609,14 +610,8 @@ StringBuffer toStringVarCond(StringBuffer sb) {
                 --countVarsNotFreeIn;
             }
 
-            int countVariableConditions = variableConditions.size();
-            for (final VariableCondition vc : variableConditions) {
-                sb.append(vc);
-                if (countVariableConditions > 0) {
-                    sb.append(", ");
-                }
-                --countVariableConditions;
-            }
+            sb.append(formatAsList(variableConditions, "", ", ", ""));
+
             sb = sb.append(")\n");
         }
         return sb;
@@ -626,29 +621,14 @@ StringBuffer toStringGoalTemplates(StringBuffer sb) {
         if (goalTemplates.isEmpty()) {
             sb.append("\\closegoal");
         } else {
-            Iterator<TacletGoalTemplate> it = goalTemplates().iterator();
-            while (it.hasNext()) {
-                sb = sb.append(it.next());
-                if (it.hasNext()) {
-                    sb = sb.append(";");
-                }
-                sb = sb.append("\n");
-            }
+            sb.append(formatAsList(goalTemplates, "", ";\n", "\n"));
         }
         return sb;
     }
 
     StringBuffer toStringRuleSets(StringBuffer sb) {
-        Iterator<RuleSet> itRS = ruleSets();
-        if (itRS.hasNext()) {
-            sb = sb.append("\\heuristics(");
-            while (itRS.hasNext()) {
-                sb = sb.append(itRS.next());
-                if (itRS.hasNext()) {
-                    sb = sb.append(", ");
-                }
-            }
-            sb = sb.append(")");
+        if (!ruleSets.isEmpty()) {
+            sb.append("\\heuristics").append(formatAsList(ruleSets, "(", ", ", ")"));
         }
         return sb;
     }
@@ -666,15 +646,8 @@ StringBuffer toStringTriggers(StringBuffer sb) {
             sb.append("} ");
             sb.append(trigger.getTerm());
             if (trigger.hasAvoidConditions()) {
-                Iterator<Term> itTerms = trigger.avoidConditions().iterator();
                 sb.append(" \\avoid ");
-                while (itTerms.hasNext()) {
-                    Term cond = itTerms.next();
-                    sb.append(cond);
-                    if (itTerms.hasNext()) {
-                        sb.append(", ");
-                    }
-                }
+                sb.append(formatAsList(trigger.avoidConditions(), "", ", ", ""));
             }
         }
         return sb;
@@ -816,9 +789,9 @@ public TacletLabelHint(TacletOperation tacletOperation, Sequent sequent) {
         }
 
         /**
-         * Constructor.
+         * Constructor creating a hint indicating
+         * {@link TacletOperation#REPLACE_TERM} as the currently performed operation.
          *
-         * @param tacletOperation The currently performed operation.
          * @param term The optional replace {@link Term} of the taclet.
          */
         public TacletLabelHint(Term term) {