Provide additional String formating utility method to reduce code dup…

…lication
KeYProject · Oct 20, 2023 · efc0f50 · efc0f50
1 parent ca0c522
commit efc0f50
Show file tree

Hide file tree

Showing 8 changed files with 114 additions and 60 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Function.java b/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().iterator(), '(', ',', ')'));
         }
         s.append(";\n");
         return s.toString();

diff --git a/key.util/src/main/java/org/key_project/util/Strings.java b/key.util/src/main/java/org/key_project/util/Strings.java
@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.util;
 
+import java.util.Iterator;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
@@ -53,4 +54,30 @@ public static boolean isJMLComment(String comment) {
             return false;
         }
     }
+
+    /**
+     * outputs the collection represented by the iterator in the format
+     * <code> open element1 sep element2 sep element3 close</code>
+     *
+     * @param it the Iterator over the collection to be printed
+     * @param open the char used as opening character
+     * @param sep the char separating the different elements
+     * @param close the char used as closing character
+     * @return the CharSequence in the described format
+     * @param <S> the type of the elements of the iterated collection
+     */
+    public static <S> String formatAsList(Iterator<S> it, char open, char sep, char close) {
+        final StringBuilder str = new StringBuilder();
+        str.append(open);
+        var hasNext = it.hasNext();
+        while (hasNext) {
+            str.append(it.next());
+            hasNext = it.hasNext();
+            if (hasNext) {
+                str.append(sep);
+            }
+        }
+        str.append(close);
+        return str.toString();
+    }
 }
diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java
@@ -5,6 +5,8 @@
 
 import java.util.Iterator;
 
+import org.key_project.util.Strings;
+
 /**
  * This class implements ImmMap<S,T> and provides a persistent Map. It is a simple implementation
  * like lists
@@ -222,16 +224,7 @@ public Iterator<ImmutableMapEntry<S, T>> iterator() {
     }
 
     public String toString() {
-        final StringBuilder sb = new StringBuilder("[");
-        final Iterator<ImmutableMapEntry<S, T>> it = iterator();
-        while (it.hasNext()) {
-            sb.append(it.next());
-            if (it.hasNext()) {
-                sb.append(",");
-            }
-        }
-        sb.append("]");
-        return sb.toString();
+        return Strings.formatAsList(iterator(), '[', ',', ']');
     }
 
     @SuppressWarnings("unchecked")

diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java
@@ -12,6 +12,8 @@
 import java.util.stream.StreamSupport;
 import javax.annotation.Nullable;
 
+import org.key_project.util.Strings;
+
 /**
  * implementation of a persistent set using the SLListOf<T> implementation with all its implications
  * (means e.g. O(n) for adding an element, searching for an element and so on).
@@ -326,16 +328,7 @@ public static <T> ImmutableSet<T> fromCollection(@Nullable Collection<T> seq) {
 
     @Override
     public String toString() {
-        Iterator<T> it = this.iterator();
-        StringBuilder str = new StringBuilder("{");
-        while (it.hasNext()) {
-            str.append(it.next());
-            if (it.hasNext()) {
-                str.append(",");
-            }
-        }
-        str.append("}");
-        return str.toString();
+        return Strings.formatAsList(iterator(), '{', ',', '}');
     }
 
     /** represents the empty set for elements of type <T> */

diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java
@@ -13,6 +13,8 @@
 import java.util.stream.StreamSupport;
 import javax.annotation.Nonnull;
 
+import org.key_project.util.Strings;
+
 public class ImmutableArray<S> implements java.lang.Iterable<S>, java.io.Serializable {
 
     /**
@@ -145,16 +147,7 @@ public boolean equals(Object o) {
 
     @Override
     public String toString() {
-        StringBuilder sb = new StringBuilder();
-        sb.append("[");
-        for (int i = 0, sz = size(); i < sz; i++) {
-            sb.append(content[i]);
-            if (i < sz - 1) {
-                sb.append(",");
-            }
-        }
-        sb.append("]");
-        return sb.toString();
+        return Strings.formatAsList(iterator(), '[', ',', ']');
     }
 
     @Override

diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java
@@ -6,6 +6,8 @@
 import java.util.ArrayDeque;
 import java.util.Iterator;
 
+import org.key_project.util.Strings;
+
 /**
  * This class implements the leftist heap, see &quot;Functional Data Structures&quot; by Chris
  * Okasaki
@@ -331,16 +333,7 @@ public Iterator<T> sortedIterator() {
 
 
     public String toString() {
-        Iterator<T> it = this.iterator();
-        StringBuilder str = new StringBuilder("[");
-        while (it.hasNext()) {
-            str.append(it.next());
-            if (it.hasNext()) {
-                str.append(",");
-            }
-        }
-        str.append("]");
-        return str.toString();
+        return Strings.formatAsList(iterator(), '[', ',', ']');
     }
 
 

diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java
@@ -12,6 +12,8 @@
 import java.util.function.Supplier;
 import java.util.stream.Collector;
 
+import org.key_project.util.Strings;
+
 /**
  * Simple implementation of a non-destructive (unmodifiable) list. The list implementation allows
  * list sharing of sublists.
@@ -451,16 +453,7 @@ public boolean equals(Object o) {
 
         @Override
         public String toString() {
-            Iterator<S> it = this.iterator();
-            StringBuilder str = new StringBuilder("[");
-            while (it.hasNext()) {
-                str.append(it.next());
-                if (it.hasNext()) {
-                    str.append(",");
-                }
-            }
-            str.append("]");
-            return str.toString();
+            return Strings.formatAsList(this.iterator(), '[', ',', ']');
         }
     }
 

diff --git a/key.util/src/test/java/org/key_project/util/StringsTest.java b/key.util/src/test/java/org/key_project/util/StringsTest.java
@@ -0,0 +1,70 @@
+/* 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.util;
+
+import java.util.Arrays;
+import java.util.Iterator;
+
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+class StringsTest {
+
+    @Test
+    void containsWholeWord() {
+        String[] sentences = new String[] {
+            "asfKeY;prover",
+            "KeY prover",
+            "KeY,prover",
+            "KeY;prover",
+            "key;prover"
+        };
+        assertTrue(Strings.containsWholeWord(sentences[0], "prover"));
+        assertFalse(Strings.containsWholeWord(sentences[0], "KeY"));
+        assertTrue(Strings.containsWholeWord(sentences[1], "prover"));
+        assertTrue(Strings.containsWholeWord(sentences[1], "KeY"));
+        assertTrue(Strings.containsWholeWord(sentences[2], "prover"));
+        assertTrue(Strings.containsWholeWord(sentences[2], "KeY"));
+        assertTrue(Strings.containsWholeWord(sentences[3], "prover"));
+        assertTrue(Strings.containsWholeWord(sentences[3], "KeY"));
+        assertTrue(Strings.containsWholeWord(sentences[4], "prover"));
+        assertFalse(Strings.containsWholeWord(sentences[4], "KeY"));
+    }
+
+    @Test
+    void isJMLComment() {
+        String[] correctComments = {
+            "/*@ requires ", "//@ requires",
+            "/*+KeY@ requires", "//+KeY@ requires",
+            "/*-OtherTool@", "//-OtherTool@"
+        };
+        String[] inCorrectComments = {
+            "/* @ requires ", "// @ requires",
+            "/*+OtherTool@ requires", "//+OtherTool@ requires",
+            "/*-KeY@", "//*-KeY@"
+        };
+
+        for (var comment : correctComments) {
+            assertTrue(Strings.isJMLComment(comment),
+                "Classified correct comment as incorrect: " + comment);
+        }
+        for (var comment : inCorrectComments) {
+            assertFalse(Strings.isJMLComment(comment),
+                "Classified incorrect comment as correct: " + comment);
+        }
+    }
+
+    @Test
+    void formatAsList() {
+        Iterator<String> it = Arrays.stream(new String[] { "a", "b", "c" }).iterator();
+        assertEquals("%a;b;c$", Strings.formatAsList(it, '%', ';', '$'));
+
+        it = Arrays.stream(new String[] { "a" }).iterator();
+        assertEquals("%a$", Strings.formatAsList(it, '%', ';', '$'));
+
+        it = Arrays.stream(new String[] {}).iterator();
+        assertEquals("%$", Strings.formatAsList(it, '%', ';', '$'));
+    }
+}