From aba5f4e27a66bd2e521d6dce311eebb9484748b9 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 20 Oct 2023 13:57:39 +0200 Subject: [PATCH 1/4] Provide additional String formating utility method to reduce code duplication --- .../de/uka/ilkd/key/logic/op/Function.java | 12 +--- .../java/org/key_project/util/Strings.java | 27 +++++++ .../util/collection/DefaultImmutableMap.java | 13 +--- .../util/collection/DefaultImmutableSet.java | 13 +--- .../util/collection/ImmutableArray.java | 13 +--- .../util/collection/ImmutableLeftistHeap.java | 13 +--- .../util/collection/ImmutableSLList.java | 13 +--- .../org/key_project/util/StringsTest.java | 70 +++++++++++++++++++ 8 files changed, 114 insertions(+), 60 deletions(-) create mode 100644 key.util/src/test/java/org/key_project/util/StringsTest.java 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 index c21e6a81edd..3ca02d25dff 100644 --- 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 index dc44b881f3e..790bfa00423 100644 --- 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 + * open element1 sep element2 sep element3 close + * + * @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 the type of the elements of the iterated collection + */ + public static String formatAsList(Iterator 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 index 0dae5e98770..9d62a9d4c83 100644 --- 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 and provides a persistent Map. It is a simple implementation * like lists @@ -222,16 +224,7 @@ public Iterator> iterator() { } public String toString() { - final StringBuilder sb = new StringBuilder("["); - final Iterator> 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 index 9401bdcea61..2fccdb274ae 100644 --- 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 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 ImmutableSet fromCollection(@Nullable Collection seq) { @Override public String toString() { - Iterator 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 */ 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 index a2920910e8d..ff42f494f95 100644 --- 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 implements java.lang.Iterable, 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 index fc4159297ac..cbceca8efec 100644 --- 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 "Functional Data Structures" by Chris * Okasaki @@ -331,16 +333,7 @@ public Iterator sortedIterator() { public String toString() { - Iterator 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 index 7379ac272ab..578cf56e03d 100644 --- 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 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 new file mode 100644 index 00000000000..da645e68a63 --- /dev/null +++ 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 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, '%', ';', '$')); + } +} From 9a44a9c41646748c80b013ec6828fc658cba7ada Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 20 Oct 2023 18:23:30 +0200 Subject: [PATCH 2/4] Replaced some additional string concatenations This fixes also a small issue in the toString method for variable conditions in taclets. --- .../reference/DefaultProofReference.java | 14 +- .../ilkd/key/util/rifl/RIFLTransformer.java | 15 +- .../AbstractUpdateExtractor.java | 14 +- .../java/de/uka/ilkd/key/logic/TermImpl.java | 27 +- .../de/uka/ilkd/key/logic/op/Function.java | 2 +- .../java/de/uka/ilkd/key/rule/Taclet.java | 47 +--- .../de/uka/ilkd/key/nparser/taclets.old.txt | 240 +++++++++--------- .../java/org/key_project/util/Strings.java | 65 ++++- .../util/collection/DefaultImmutableMap.java | 2 +- .../util/collection/DefaultImmutableSet.java | 2 +- .../util/collection/ImmutableArray.java | 2 +- .../util/collection/ImmutableLeftistHeap.java | 2 +- .../util/collection/ImmutableSLList.java | 2 +- .../org/key_project/util/StringsTest.java | 17 +- 14 files changed, 225 insertions(+), 226 deletions(-) diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java index 968c82d4296..18fe6e1daf1 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java +++ b/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 implements IProofReference { * 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 \""); diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java index e702cda69d7..d76a95c697a 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java +++ b/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 @@ public void doTransform(final File riflFilename, final File source, final File s 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"; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java index b700410c009..6bce16badaa 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java +++ b/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 @@ public ImmutableList getStartingGoals() { */ @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).andThen(Node::serialNr))); return sb.toString(); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java index 4318d253541..25e7c2eb5a4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java +++ b/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 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 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 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(); 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 index 3ca02d25dff..4e1a5795998 100644 --- 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 @@ -116,7 +116,7 @@ public final String proofToString() { new StringBuilder((sort() == Sort.FORMULA ? "" : sort().toString()) + " "); s.append(name()); if (arity() > 0) { - s.append(Strings.formatAsList(argSorts().iterator(), '(', ',', ')')); + s.append(Strings.formatAsList(argSorts().iterator(), "(", ",", ")")); } s.append(";\n"); return s.toString(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java index 52e26d93f6d..f59a1ede150 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java +++ b/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 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 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 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) { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index 0a524fb943d..3f697ff552c 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1,5 +1,5 @@ # This files contains representation of taclets, which are accepted and revised. -# Date: Tue Jul 25 17:12:50 CEST 2023 +# Date: Fri Oct 20 19:55:38 CEST 2023 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) ========================================= abortJavaCardTransactionAPI { @@ -678,7 +678,7 @@ allocateInstance { \find(==>#allmodal ( (modal operator))\[{ .. #lhs = #t.#allocate()@#t; ... }\] (post)) -\varcond(\hasSort(#t2 (program Type), alphaObj), ) +\varcond(\hasSort(#t2 (program Type), alphaObj)) \add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),equals(boolean::select(heap,#lhs,java.lang.Object::),FALSE))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(create(heap,#lhs)),#allmodal(post))]) \heuristics(method_expand) Choices: (programRules:Java & permissions:off)} @@ -688,7 +688,7 @@ allocateInstanceWithLength { \find(==>#allmodal ( (modal operator))\[{ .. #lhs = #t.#allocate(#len)@#t; ... }\] (post)) -\varcond(\hasSort(#t2 (program Type), alphaObj), ) +\varcond(\hasSort(#t2 (program Type), alphaObj)) \add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),and(equals(boolean::select(heap,#lhs,java.lang.Object::),FALSE),equals(length(#lhs),#len)))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(store(store(create(heap,#lhs),#lhs,java.lang.Object::,Z(0(#))),#lhs,java.lang.Object::,FALSE)),#allmodal(post))]) \heuristics(method_expand) Choices: (programRules:Java & permissions:off)} @@ -938,7 +938,7 @@ Choices: true} == applyOnRigidFormula (applyOnRigidFormula) ========================================= applyOnRigidFormula { \find(update-application(u,phi)) -\varcond(\applyUpdateOnRigid(u (update), phi (formula), result (formula)), ) +\varcond(\applyUpdateOnRigid(u (update), phi (formula), result (formula))) \replacewith(result) \heuristics(update_apply) Choices: true} @@ -946,7 +946,7 @@ Choices: true} == applyOnRigidTerm (applyOnRigidTerm) ========================================= applyOnRigidTerm { \find(update-application(u,t)) -\varcond(\applyUpdateOnRigid(u (update), t (any term), result (any term)), ) +\varcond(\applyUpdateOnRigid(u (update), t (any term), result (any term))) \replacewith(result) \heuristics(update_apply) Choices: true} @@ -1156,7 +1156,7 @@ Choices: programRules:Java} array_store_known_dynamic_array_type { \assumes ([equals(J::exactInstance(array),TRUE)]==>[]) \find(arrayStoreValid(array,obj)) -\sameUpdateLevel\varcond(\isReference[non_null]( J ), ) +\sameUpdateLevel\varcond(\isReference[non_null]( J )) \replacewith(or(equals(obj,null),equals(#arrayBaseInstanceOf(J::exactInstance(array),obj),TRUE))) \heuristics(simplify) Choices: programRules:Java} @@ -1187,7 +1187,7 @@ assertSafe { \find(==>#allmodal ( (modal operator))\[{ .. assert #e1; ... }\] (b)) -\varcond(\new(#condition (program Variable), \typeof(#e1 (program Expression))), \not \containsAssignment( #e1 ), ) +\varcond(\new(#condition (program Variable), \typeof(#e1 (program Expression))), \not \containsAssignment( #e1 )) \add [equals(oldHeap,heap)]==>[] \replacewith([]==>[\[{ method-frame (#ex) { #typeof(#e1) #condition = #e1; @@ -1207,7 +1207,7 @@ assertSafeWithMessage { \find(==>#allmodal ( (modal operator))\[{ .. assert #e1 : #e2; ... }\] (b)) -\varcond(\new(#message (program Variable), \typeof(#e2 (program Expression))), \new(#condition (program Variable), \typeof(#e1 (program Expression))), \not \containsAssignment( #e1 ), \not \containsAssignment( #e2 ), ) +\varcond(\new(#message (program Variable), \typeof(#e2 (program Expression))), \new(#condition (program Variable), \typeof(#e1 (program Expression))), \not \containsAssignment( #e1 ), \not \containsAssignment( #e2 )) \add [equals(oldHeap,heap)]==>[] \replacewith([]==>[\[{ method-frame (#ex) { #typeof(#e1) #condition = #e1; @@ -1264,7 +1264,7 @@ assignmentAdditionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 + #seDouble1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1274,7 +1274,7 @@ assignmentAdditionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 + #seDouble1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(addDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1284,7 +1284,7 @@ assignmentAdditionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 + #seFloat1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1294,7 +1294,7 @@ assignmentAdditionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 + #seFloat1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(addFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1468,7 +1468,7 @@ assignmentDivisionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 / #seDouble1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1478,7 +1478,7 @@ assignmentDivisionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 / #seDouble1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(divDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1488,7 +1488,7 @@ assignmentDivisionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 / #seFloat1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1498,7 +1498,7 @@ assignmentDivisionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 / #seFloat1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(divFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1604,7 +1604,7 @@ assignmentMultiplicationDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 * #seDouble1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1614,7 +1614,7 @@ assignmentMultiplicationDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 * #seDouble1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(mulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1624,7 +1624,7 @@ assignmentMultiplicationFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 * #seFloat1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1634,7 +1634,7 @@ assignmentMultiplicationFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 * #seFloat1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(mulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1734,7 +1734,7 @@ assignmentSubtractionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 - #seDouble1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1744,7 +1744,7 @@ assignmentSubtractionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 - #seDouble1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(subDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1754,7 +1754,7 @@ assignmentSubtractionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 - #seFloat1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1764,7 +1764,7 @@ assignmentSubtractionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 - #seFloat1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp) \replacewith(update-application(elem-update(#loc (program Variable))(subFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1828,7 +1828,7 @@ assignment_array2 { \find(==>#allmodal ( (modal operator))\[{ .. #v = #v0[#se]; ... }\] (post)) -\varcond(\hasSort(\elemSort(#v0 (program Variable)), G), ) +\varcond(\hasSort(\elemSort(#v0 (program Variable)), G)) \add [and(not(equals(#v0,null)),or(leq(length(#v0),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v0,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(#v (program Variable))(G::select(heap,#v0,arr(#se))),#allmodal(post))]) @@ -1840,7 +1840,7 @@ assignment_read_attribute { \find(==>#allmodal ( (modal operator))\[{ .. #v0 = #v.#a; ... }\] (post)) -\varcond( \not \static(#a (program Variable)), \not \isArrayLength(#a (program Variable)), \not\isModelField(#a (program Variable)), \hasSort(#a (program Variable), G), \not\isThisReference (#v (program Variable)), ) +\varcond( \not \static(#a (program Variable)), \not \isArrayLength(#a (program Variable)), \not\isModelField(#a (program Variable)), \hasSort(#a (program Variable), G), \not\isThisReference (#v (program Variable))) \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(#v0 (program Variable))(G::select(heap,#v,#memberPVToField(#a))),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) @@ -1851,7 +1851,7 @@ assignment_read_attribute_this { \find(==>#allmodal ( (modal operator))\[{ .. #v0 = #v.#a; ... }\] (post)) -\varcond( \not \static(#a (program Variable)), \not \isArrayLength(#a (program Variable)), \not\isModelField(#a (program Variable)), \hasSort(#a (program Variable), G), \isThisReference (#v (program Variable)), ) +\varcond( \not \static(#a (program Variable)), \not \isArrayLength(#a (program Variable)), \not\isModelField(#a (program Variable)), \hasSort(#a (program Variable), G), \isThisReference (#v (program Variable))) \replacewith([]==>[update-application(elem-update(#v0 (program Variable))(G::select(heap,#v,#memberPVToField(#a))),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & runtimeExceptions:ban)} @@ -1861,7 +1861,7 @@ assignment_read_length { \find(==>#allmodal ( (modal operator))\[{ .. #v0 = #v.#length; ... }\] (post)) -\varcond(\not\isThisReference (#v (program Variable)), ) +\varcond(\not\isThisReference (#v (program Variable))) \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(#v0 (program Variable))(length(#v)),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) @@ -1872,7 +1872,7 @@ assignment_read_length_this { \find(#allmodal ( (modal operator))\[{ .. #v0 = #v.#length; ... }\] (post)) -\sameUpdateLevel\varcond(\isThisReference (#v (program Variable)), ) +\sameUpdateLevel\varcond(\isThisReference (#v (program Variable))) \replacewith(update-application(elem-update(#v0 (program Variable))(length(#v)),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java} @@ -1882,7 +1882,7 @@ assignment_read_static_attribute { \find(#allmodal ( (modal operator))\[{ .. #v0 = @(#sv); ... }\] (post)) -\sameUpdateLevel\varcond(\hasSort(#sv (program StaticVariable), G), ) +\sameUpdateLevel\varcond(\hasSort(#sv (program StaticVariable), G)) \replacewith(update-application(elem-update(#v0 (program Variable))(G::select(heap,null,#memberPVToField(#sv))),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java} @@ -1892,7 +1892,7 @@ assignment_read_static_attribute_with_variable_prefix { \find(#allmodal ( (modal operator))\[{ .. #loc = @(#v.#sv); ... }\] (post)) -\varcond(\hasSort(#sv (program StaticVariable), G), ) +\varcond(\hasSort(#sv (program StaticVariable), G)) \replacewith(update-application(elem-update(#loc (program Variable))(G::select(heap,#v,#memberPVToField(#sv))),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java} @@ -1902,7 +1902,7 @@ assignment_to_primitive_array_component { \find(==>#normal ( (modal operator))\[{ .. #v[#se] = #se0; ... }\] (post)) -\varcond( \not \isReferenceArray(#v (program Variable)), ) +\varcond( \not \isReferenceArray(#v (program Variable))) \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),#normal(post))]) @@ -1914,7 +1914,7 @@ assignment_to_primitive_array_component_transaction { \find(==>#transaction ( (modal operator))\[{ .. #v[#se] = #se0; ... }\] (post)) -\varcond( \not \isReferenceArray(#v (program Variable)), ) +\varcond( \not \isReferenceArray(#v (program Variable))) \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::),Z(0(#))),store(savedHeap,#v,java.lang.Object::,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) @@ -1926,7 +1926,7 @@ assignment_to_reference_array_component { \find(==>#normal ( (modal operator))\[{ .. #v[#se] = #se0; ... }\] (post)) -\varcond(\isReferenceArray(#v (program Variable)), ) +\varcond(\isReferenceArray(#v (program Variable))) \add [and(and(and(not(equals(#v,null)),lt(#se,length(#v))),geq(#se,Z(0(#)))),not(arrayStoreValid(#v,#se0)))]==>[] \replacewith([]==>[false]) ; \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; @@ -1939,7 +1939,7 @@ assignment_to_reference_array_component_transaction { \find(==>#transaction ( (modal operator))\[{ .. #v[#se] = #se0; ... }\] (post)) -\varcond(\isReferenceArray(#v (program Variable)), ) +\varcond(\isReferenceArray(#v (program Variable))) \add [and(and(and(not(equals(#v,null)),lt(#se,length(#v))),geq(#se,Z(0(#)))),not(arrayStoreValid(#v,#se0)))]==>[] \replacewith([]==>[false]) ; \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; @@ -1961,7 +1961,7 @@ assignment_write_attribute { \find(==>#allmodal ( (modal operator))\[{ .. #v.#a = #se; ... }\] (post)) -\varcond( \not \static(#a (program Variable)), \not\isThisReference (#v (program Variable)), ) +\varcond( \not \static(#a (program Variable)), \not\isThisReference (#v (program Variable))) \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,#memberPVToField(#a),#se)),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) @@ -1972,7 +1972,7 @@ assignment_write_attribute_this { \find(==>#allmodal ( (modal operator))\[{ .. #v.#a = #se; ... }\] (post)) -\varcond( \not \static(#a (program Variable)), \isThisReference (#v (program Variable)), ) +\varcond( \not \static(#a (program Variable)), \isThisReference (#v (program Variable))) \replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,#memberPVToField(#a),#se)),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & runtimeExceptions:ban)} @@ -3418,7 +3418,7 @@ Choices: true} castAdd2 { \assumes ([equals(cs,gt)]==>[]) \find(gt) -\sameUpdateLevel\varcond(\strict\sub(C, G), ) +\sameUpdateLevel\varcond(\strict\sub(C, G)) \replacewith(C::cast(gt)) Choices: true} @@ -5169,7 +5169,7 @@ Choices: programRules:Java} == createdInHeapWithObserver (createdInHeapWithObserver) ========================================= createdInHeapWithObserver { \find(==>createdInHeap(obs,h)) -\varcond(\isObserver (obs (LocSet term), h (Heap term)), ) +\varcond(\isObserver (obs (LocSet term), h (Heap term))) \replacewith([]==>[wellFormed(h)]) \heuristics(concrete) Choices: programRules:Java} @@ -5178,7 +5178,7 @@ Choices: programRules:Java} createdInHeapWithObserverEQ { \assumes ([equals(obs,EQ)]==>[]) \find(==>createdInHeap(EQ,h)) -\varcond(\isObserver (obs (LocSet term), h (Heap term)), ) +\varcond(\isObserver (obs (LocSet term), h (Heap term))) \replacewith([]==>[wellFormed(h)]) \heuristics(concrete) Choices: programRules:Java} @@ -5507,7 +5507,7 @@ delete_unnecessary_cast { \find(#allmodal ( (modal operator))\[{ .. #lhs = (#npit) #se; ... }\] (post)) -\sameUpdateLevel\varcond(\hasSort(#npit (program NonPrimitiveType), G), \sub(\typeof(#se (program SimpleExpression)), G), ) +\sameUpdateLevel\varcond(\hasSort(#npit (program NonPrimitiveType), G), \sub(\typeof(#se (program SimpleExpression)), G)) \add [or(equals(#se,null),equals(G::instance(#se),TRUE))]==>[] \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(#addCast(#se,#lhs)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java} @@ -5772,7 +5772,7 @@ Choices: programRules:Java} == dismissNonSelectedField (dismissNonSelectedField) ========================================= dismissNonSelectedField { \find(alpha::select(store(h,o,f1,x),u,f2)) -\varcond(\differentFields (f1 (Field term), f2 (Field term)), ) +\varcond(\differentFields (f1 (Field term), f2 (Field term))) \replacewith(alpha::select(h,u,f2)) \heuristics(simplify) Choices: programRules:Java} @@ -5781,7 +5781,7 @@ Choices: programRules:Java} dismissNonSelectedFieldEQ { \assumes ([equals(store(h,o,f1,x),EQ)]==>[]) \find(alpha::select(EQ,u,f2)) -\sameUpdateLevel\varcond(\differentFields (f1 (Field term), f2 (Field term)), ) +\sameUpdateLevel\varcond(\differentFields (f1 (Field term), f2 (Field term))) \replacewith(alpha::select(h,u,f2)) \heuristics(simplify) Choices: programRules:Java} @@ -6159,7 +6159,7 @@ doWhileUnwind { do #s while (#e); ... }\] (post)) -\varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label)), ) +\varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label))) \replacewith(#allmodal ( (modal operator))\[{ .. #unwind-loop(do #s while (#e);) @@ -6193,7 +6193,7 @@ Choices: true} == dropEffectlessStores (dropEffectlessStores) ========================================= dropEffectlessStores { \find(store(h,o,f,x)) -\varcond(\dropEffectlessStores(h (Heap term), o (java.lang.Object term), f (Field term), x (any term), result (Heap term)), ) +\varcond(\dropEffectlessStores(h (Heap term), o (java.lang.Object term), f (Field term), x (any term), result (Heap term))) \replacewith(result) \heuristics(concrete) Choices: programRules:Java} @@ -6274,7 +6274,7 @@ Choices: programRules:Java} ----------------------------------------------------- == elementOfInfiniteUnion2Vars (elementOfInfiniteUnion2Vars) ========================================= elementOfInfiniteUnion2Vars { -\find(elementOf(o,f,infiniteUnion{av (variable), bv (variable)}(s))) +\find(elementOf(o,f,infiniteUnion{av (variable),bv (variable)}(s))) \varcond(\notFreeIn(bv (variable), f (Field term)), \notFreeIn(bv (variable), o (java.lang.Object term)), \notFreeIn(av (variable), f (Field term)), \notFreeIn(av (variable), o (java.lang.Object term))) \replacewith(exists{av (variable)}(exists{bv (variable)}(elementOf(o,f,s)))) \heuristics(simplify) @@ -6282,7 +6282,7 @@ Choices: programRules:Java} ----------------------------------------------------- == elementOfInfiniteUnion2VarsEQ (elementOfInfiniteUnion2VarsEQ) ========================================= elementOfInfiniteUnion2VarsEQ { -\assumes ([equals(infiniteUnion{av (variable), bv (variable)}(s),EQ)]==>[]) +\assumes ([equals(infiniteUnion{av (variable),bv (variable)}(s),EQ)]==>[]) \find(elementOf(o,f,EQ)) \sameUpdateLevel\varcond(\notFreeIn(bv (variable), f (Field term)), \notFreeIn(bv (variable), o (java.lang.Object term)), \notFreeIn(av (variable), f (Field term)), \notFreeIn(av (variable), o (java.lang.Object term))) \replacewith(exists{av (variable)}(exists{bv (variable)}(elementOf(o,f,s)))) @@ -7100,7 +7100,7 @@ Choices: Strings:on} == equalUnique (equalUnique) ========================================= equalUnique { \find(equals(f,f2)) -\varcond(\equalUnique (f (any term), f2 (any term), result (formula)), ) +\varcond(\equalUnique (f (any term), f2 (any term), result (formula))) \replacewith(result) \heuristics(concrete) Choices: true} @@ -7395,7 +7395,7 @@ eval_order_access4 { \find(#allmodal ( (modal operator))\[{ .. #v.#a = #nse; ... }\] (post)) -\varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#v (program Variable))), \not \static(#a (program Variable)), ) +\varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#v (program Variable))), \not \static(#a (program Variable))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#v) #v0 = #v; #typeof(#nse) #v1 = #nse; @@ -7409,7 +7409,7 @@ eval_order_access4_this { \find(#allmodal ( (modal operator))\[{ .. #v.#a = #nse; ... }\] (post)) -\varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \not \static(#a (program Variable)), \isThisReference (#v (program Variable)), ) +\varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \not \static(#a (program Variable)), \isThisReference (#v (program Variable))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v1 = #nse; #v.#a = #v1; @@ -7964,7 +7964,7 @@ Choices: programRules:Java} == exact_instance_for_interfaces_or_abstract_classes (interfaces or abstract classes have no exact instances) ========================================= exact_instance_for_interfaces_or_abstract_classes { \find(G::exactInstance(obj)) -\varcond(\isAbstractOrInterface (G), ) +\varcond(\isAbstractOrInterface (G)) \replacewith(FALSE) \heuristics(simplify) Choices: programRules:Java} @@ -7973,7 +7973,7 @@ Choices: programRules:Java} exact_instance_known_dynamic_type { \assumes ([equals(G::exactInstance(a),TRUE)]==>[]) \find(H::exactInstance(a)) -\sameUpdateLevel\varcond(\not\same(G, H), ) +\sameUpdateLevel\varcond(\not\same(G, H)) \replacewith(FALSE) \heuristics(evaluate_instanceof, simplify) Choices: true} @@ -8168,7 +8168,7 @@ execBreakLabelEliminateBreakLabelNoMatch { #slist1 }#cs ... }\] (post)) -\varcond(\different (#lb (program Label), #lb1 (program Label)), ) +\varcond(\different (#lb (program Label), #lb1 (program Label))) \replacewith(#allmodal ( (modal operator))\[{ .. exec { break; @@ -8557,7 +8557,7 @@ execContinueLabelEliminateContinueLabelNoMatch { #slist1 }#cs ... }\] (post)) -\varcond(\different (#lb (program Label), #lb1 (program Label)), ) +\varcond(\different (#lb (program Label), #lb1 (program Label))) \replacewith(#allmodal ( (modal operator))\[{ .. exec { continue; @@ -8888,7 +8888,7 @@ execReturnVal { #slist1 }#cs ... }\] (post)) -\varcond(\sub(\typeof(#se (program SimpleExpression)), \typeof(#v (program Variable))), ) +\varcond(\sub(\typeof(#se (program SimpleExpression)), \typeof(#v (program Variable)))) \replacewith(#allmodal ( (modal operator))\[{ .. { #t #v; @@ -9053,7 +9053,7 @@ execReturnValNonMatchingType { #slist1 }#cs ... }\] (post)) -\varcond(\not\sub(\typeof(#se (program SimpleExpression)), \typeof(#v (program Variable))), ) +\varcond(\not\sub(\typeof(#se (program SimpleExpression)), \typeof(#v (program Variable)))) \replacewith(#allmodal ( (modal operator))\[{ .. exec { return #se; @@ -9475,7 +9475,7 @@ for_to_while { \find(#allmodal ( (modal operator))\[{ .. #forloop ... }\] (post)) -\varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label)), ) +\varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label))) \replacewith(#allmodal ( (modal operator))\[{ .. #for-to-while(#forloop) ... }\] (post)) @@ -11389,7 +11389,7 @@ Choices: programRules:Java} instanceof_known_dynamic_type { \assumes ([equals(G::exactInstance(a),TRUE)]==>[]) \find(H::instance(a)) -\sameUpdateLevel\varcond(\sub(G, H), ) +\sameUpdateLevel\varcond(\sub(G, H)) \replacewith(TRUE) \heuristics(evaluate_instanceof, simplify) Choices: true} @@ -11398,7 +11398,7 @@ Choices: true} instanceof_known_dynamic_type_2 { \assumes ([equals(G::exactInstance(a),TRUE)]==>[]) \find(H::instance(a)) -\sameUpdateLevel\varcond(\not\sub(G, H), ) +\sameUpdateLevel\varcond(\not\sub(G, H)) \replacewith(FALSE) \heuristics(evaluate_instanceof, simplify) Choices: true} @@ -11406,7 +11406,7 @@ Choices: true} == instanceof_not_compatible (instanceof disjoint type) ========================================= instanceof_not_compatible { \find(equals(G::instance(a),TRUE)) -\varcond(\sub(Null, G), \disjointModuloNull(G, \typeof(a (any term))), ) +\varcond(\sub(Null, G), \disjointModuloNull(G, \typeof(a (any term)))) \replacewith(equals(a,null)) \heuristics(evaluate_instanceof, concrete) Choices: true} @@ -11414,7 +11414,7 @@ Choices: true} == instanceof_not_compatible_2 (instanceof disjoint type) ========================================= instanceof_not_compatible_2 { \find(equals(G::instance(a),FALSE)) -\varcond(\sub(Null, G), \disjointModuloNull(G, \typeof(a (any term))), ) +\varcond(\sub(Null, G), \disjointModuloNull(G, \typeof(a (any term)))) \replacewith(not(equals(a,null))) \heuristics(evaluate_instanceof, concrete) Choices: true} @@ -11422,7 +11422,7 @@ Choices: true} == instanceof_not_compatible_3 (instanceof disjoint type) ========================================= instanceof_not_compatible_3 { \find(equals(G::instance(a),TRUE)) -\varcond(\not\sub(Null, G), \disjointModuloNull(G, \typeof(a (any term))), ) +\varcond(\not\sub(Null, G), \disjointModuloNull(G, \typeof(a (any term)))) \replacewith(false) \heuristics(evaluate_instanceof, concrete) Choices: true} @@ -11430,7 +11430,7 @@ Choices: true} == instanceof_not_compatible_4 (instanceof disjoint type) ========================================= instanceof_not_compatible_4 { \find(equals(G::instance(a),FALSE)) -\varcond(\not\sub(Null, G), \disjointModuloNull(G, \typeof(a (any term))), ) +\varcond(\not\sub(Null, G), \disjointModuloNull(G, \typeof(a (any term)))) \replacewith(true) \heuristics(evaluate_instanceof, concrete) Choices: true} @@ -11439,7 +11439,7 @@ Choices: true} instanceof_not_compatible_5 { \assumes ([equals(H::instance(a),TRUE)]==>[]) \find(equals(G::instance(a),TRUE)) -\varcond(\sub(Null, G), \disjointModuloNull(G, H), ) +\varcond(\sub(Null, G), \disjointModuloNull(G, H)) \replacewith(equals(a,null)) \heuristics(evaluate_instanceof, concrete) Choices: true} @@ -11447,7 +11447,7 @@ Choices: true} == instanceof_static_type (instanceof static supertype) ========================================= instanceof_static_type { \find(G::instance(a)) -\varcond(\sub(\typeof(a (any term)), G), ) +\varcond(\sub(\typeof(a (any term)), G)) \replacewith(TRUE) \heuristics(evaluate_instanceof, concrete) Choices: true} @@ -11456,7 +11456,7 @@ Choices: true} instanceof_static_type_2 { \assumes ([equals(a2,a)]==>[]) \find(G::instance(a)) -\sameUpdateLevel\varcond(\sub(\typeof(a2 (any term)), G), ) +\sameUpdateLevel\varcond(\sub(\typeof(a2 (any term)), G)) \replacewith(TRUE) \heuristics(evaluate_instanceof, concrete) Choices: true} @@ -12553,7 +12553,7 @@ loopScopeInvBox { while (#nse) #body }\] (post))), \varcond (\storeStmtIn(#loopStmt (program Statement), #box ( (modal operator))\[{ while (#nse) #body -}\] (post))), \hasInvariant(#loopStmt (program Statement)), \getInvariant(#loopStmt (program Statement), #box ( (modal operator)), inv (formula)), \getFreeInvariant(#loopStmt (program Statement), #box ( (modal operator)), freeInv (formula)), ) +}\] (post))), \hasInvariant(#loopStmt (program Statement)), \getInvariant(#loopStmt (program Statement), #box ( (modal operator)), inv (formula)), \getFreeInvariant(#loopStmt (program Statement), #box ( (modal operator)), freeInv (formula))) \add [#wellFormedCond(loopFormula,anon_heap_LOOP,anon_savedHeap_LOOP,anon_permissions_LOOP)]==>[] \replacewith(#box ( (modal operator))\[{ #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; @@ -12582,7 +12582,7 @@ loopScopeInvDia { while (#nse) #body }\] (post))), \varcond (\storeStmtIn(#loopStmt (program Statement), #dia ( (modal operator))\[{ while (#nse) #body -}\] (post))), \hasInvariant(#loopStmt (program Statement)), \getInvariant(#loopStmt (program Statement), #dia ( (modal operator)), inv (formula)), \getFreeInvariant(#loopStmt (program Statement), #dia ( (modal operator)), freeInv (formula)), \getVariant(#loopStmt (program Statement), variantTerm (any term)), ) +}\] (post))), \hasInvariant(#loopStmt (program Statement)), \getInvariant(#loopStmt (program Statement), #dia ( (modal operator)), inv (formula)), \getFreeInvariant(#loopStmt (program Statement), #dia ( (modal operator)), freeInv (formula)), \getVariant(#loopStmt (program Statement), variantTerm (any term))) \add [#wellFormedCond(loopFormula,anon_heap_LOOP,anon_savedHeap_LOOP,anon_permissions_LOOP)]==>[] \replacewith(#dia ( (modal operator))\[{ #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; @@ -12608,7 +12608,7 @@ loopUnwind { \find(#allmodal ( (modal operator))\[{ .. while (#e) #s ... }\] (post)) -\varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label)), ) +\varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label))) \replacewith(#allmodal ( (modal operator))\[{ .. #unwind-loop(while (#e) #s) ... }\] (post)) @@ -12684,7 +12684,7 @@ lsLblContinueNoMatch1 { continue; #slist } -}\] (post))), \varcond (\not\isLabeled(#lsStmt (program Statement)), ) +}\] (post))), \varcond (\not\isLabeled(#lsStmt (program Statement))) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs = true; continue; @@ -12701,7 +12701,7 @@ lsLblContinueNoMatch2 { #slist } ... }\] (post)) -\varcond(\different (#lb1 (program Label), #lb (program Label)), ) +\varcond(\different (#lb1 (program Label), #lb (program Label))) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs = true; continue; @@ -12896,7 +12896,7 @@ methodCall { \find(==>#allmodal ( (modal operator))\[{ .. #se.#mn(#selist); ... }\] (post)) -\varcond(\not \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), \mayExpandMethod(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), ) +\varcond(\not \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), \mayExpandMethod(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression))) \add [equals(#se,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[#allmodal ( (modal operator))\[{ .. method-call(#se.#mn(#selist)) @@ -12942,7 +12942,7 @@ methodCallParamThrow { #slist } ... }\] (post)) -\varcond(\isLocalVariable (#se (program SimpleExpression)), ) +\varcond(\isLocalVariable (#se (program SimpleExpression))) \replacewith(#allmodal ( (modal operator))\[{ .. throw #se; ... }\] (post)) @@ -12996,7 +12996,7 @@ methodCallThrow { #slist } ... }\] (post)) -\varcond(\isLocalVariable (#se (program SimpleExpression)), ) +\varcond(\isLocalVariable (#se (program SimpleExpression))) \replacewith(#allmodal ( (modal operator))\[{ .. throw #se; ... }\] (post)) @@ -13033,7 +13033,7 @@ methodCallWithAssignment { \find(==>#allmodal ( (modal operator))\[{ .. #lhs = #se.#mn(#selist); ... }\] (post)) -\varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \not \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), \mayExpandMethod(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), ) +\varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \not \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), \mayExpandMethod(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression))) \add [equals(#se,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #typeof(#lhs) #v0; @@ -13087,7 +13087,7 @@ methodCallWithAssignmentWithinClass { \find(#allmodal ( (modal operator))\[{ .. #lhs = #mn(#elist); ... }\] (post)) -\varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \mayExpandMethod(null, #mn (program MethodName), #elist (program Expression)), ) +\varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \mayExpandMethod(null, #mn (program MethodName), #elist (program Expression))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs) #v0; method-call(#mn(#elist)) @@ -13101,7 +13101,7 @@ methodCallWithinClass { \find(#allmodal ( (modal operator))\[{ .. #mn(#elist); ... }\] (post)) -\varcond(\mayExpandMethod(null, #mn (program MethodName), #elist (program Expression)), ) +\varcond(\mayExpandMethod(null, #mn (program MethodName), #elist (program Expression))) \replacewith(#allmodal ( (modal operator))\[{ .. method-call(#mn(#elist)) ... }\] (post)) @@ -13466,7 +13466,7 @@ Choices: integerSimplificationRules:full} narrowSelectArrayType { \assumes ([wellFormed(h)]==>[equals(o,null)]) \find(beta::select(h,o,arr(idx))) -\sameUpdateLevel\varcond(\hasSort(\elemSort(o (java.lang.Object term)), alpha), \strict\sub(alpha, beta), ) +\sameUpdateLevel\varcond(\hasSort(\elemSort(o (java.lang.Object term)), alpha), \strict\sub(alpha, beta)) \replacewith(alpha::select(h,o,arr(idx))) \heuristics(simplify) Choices: programRules:Java} @@ -13475,7 +13475,7 @@ Choices: programRules:Java} narrowSelectType { \assumes ([wellFormed(h)]==>[]) \find(beta::select(h,o,f)) -\varcond(\fieldType(f (Field term), alpha), \strict\sub(alpha, beta), ) +\varcond(\fieldType(f (Field term), alpha), \strict\sub(alpha, beta)) \replacewith(alpha::select(h,o,f)) \heuristics(simplify) Choices: programRules:Java} @@ -13777,7 +13777,7 @@ Choices: programRules:Java} == nonNull (nonNull) ========================================= nonNull { \find(nonNull(heapSV,o,depth)) -\varcond(\notFreeIn(i (variable), depth (int term)), \notFreeIn(i (variable), heapSV (Heap term)), \notFreeIn(i (variable), o (java.lang.Object term)), \isReferenceArray(o (java.lang.Object term)), ) +\varcond(\notFreeIn(i (variable), depth (int term)), \notFreeIn(i (variable), heapSV (Heap term)), \notFreeIn(i (variable), o (java.lang.Object term)), \isReferenceArray(o (java.lang.Object term))) \replacewith(and(not(equals(o,null)),imp(gt(depth,Z(0(#))),all{i (variable)}(imp(and(leq(Z(0(#)),i),lt(i,length(o))),nonNull(heapSV,java.lang.Object::select(heapSV,o,arr(i)),sub(depth,Z(1(#))))))))) \heuristics(simplify_enlarging) Choices: programRules:Java} @@ -13834,7 +13834,7 @@ Choices: true} null_can_always_be_stored_in_a_reference_type_array { \assumes ([]==>[equals(array,null)]) \find(arrayStoreValid(array,null)) -\sameUpdateLevel\varcond(\isReferenceArray(array (GOS term)), ) +\sameUpdateLevel\varcond(\isReferenceArray(array (GOS term))) \replacewith(true) \heuristics(simplify) Choices: programRules:Java} @@ -13842,7 +13842,7 @@ Choices: programRules:Java} == observerDependency (observerDependency) ========================================= observerDependency { \find(termWithLargeHeap) -\inSequentState\varcond(\sameObserver (termWithLargeHeap (any term), termWithSmallHeap (any term)), ) +\inSequentState\varcond(\sameObserver (termWithLargeHeap (any term), termWithSmallHeap (any term))) \add []==>[#ObserverEquality(termWithLargeHeap,termWithSmallHeap)] ; \replacewith(termWithSmallHeap) @@ -13851,7 +13851,7 @@ Choices: programRules:Java} == observerDependencyEQ (observerDependencyEQ) ========================================= observerDependencyEQ { \find(equals(t1,t2)) -\inSequentState\varcond(\sameObserver (t1 (any term), t2 (any term)), ) +\inSequentState\varcond(\sameObserver (t1 (any term), t2 (any term))) \add []==>[#ObserverEquality(t1,t2)] ; \replacewith(true) @@ -13860,7 +13860,7 @@ Choices: programRules:Java} == observerDependencyEquiv (observerDependencyEQ) ========================================= observerDependencyEquiv { \find(equiv(t1,t2)) -\inSequentState\varcond(\sameObserver (t1 (formula), t2 (formula)), ) +\inSequentState\varcond(\sameObserver (t1 (formula), t2 (formula))) \add []==>[#ObserverEquality(t1,t2)] ; \replacewith(true) @@ -13869,7 +13869,7 @@ Choices: programRules:Java} == observerDependencyFormula (observerDependency) ========================================= observerDependencyFormula { \find(termWithLargeHeap) -\inSequentState\varcond(\sameObserver (termWithLargeHeap (formula), termWithSmallHeap (formula)), ) +\inSequentState\varcond(\sameObserver (termWithLargeHeap (formula), termWithSmallHeap (formula))) \add []==>[#ObserverEquality(termWithLargeHeap,termWithSmallHeap)] ; \replacewith(termWithSmallHeap) @@ -13894,7 +13894,7 @@ Choices: programRules:Java} == onlyCreatedObjectsAreObserved (onlyCreatedObjectsAreObserved) ========================================= onlyCreatedObjectsAreObserved { \find(obs) -\sameUpdateLevel\varcond(\isObserver (obs (deltaObject term), h (Heap term)), ) +\sameUpdateLevel\varcond(\isObserver (obs (deltaObject term), h (Heap term))) \add [or(equals(obs,null),equals(boolean::select(h,obs,java.lang.Object::),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} @@ -13902,7 +13902,7 @@ Choices: programRules:Java} == onlyCreatedObjectsAreObservedInLocSets (onlyCreatedObjectsAreObservedInLocSets) ========================================= onlyCreatedObjectsAreObservedInLocSets { \find(elementOf(o,f,obs)==>) -\varcond(\isObserver (obs (LocSet term), h (Heap term)), ) +\varcond(\isObserver (obs (LocSet term), h (Heap term))) \add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} @@ -13911,7 +13911,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreObservedInLocSetsEQ { \assumes ([equals(obs,EQ)]==>[]) \find(elementOf(o,f,EQ)==>) -\varcond(\isObserver (obs (LocSet term), h (Heap term)), ) +\varcond(\isObserver (obs (LocSet term), h (Heap term))) \add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} @@ -14935,7 +14935,7 @@ Choices: reach:on} == reachDependenciesStoreSimple (reachDependenciesStoreSimple) ========================================= reachDependenciesStoreSimple { \find(reach(store(h,o3,f2,x),allObjects(f),o,o2,n)) -\varcond(\metaDisjoint f (Field term), f2 (Field term), ) +\varcond(\metaDisjoint f (Field term), f2 (Field term)) \replacewith(reach(h,allObjects(f),o,o2,n)) \heuristics(simplify) Choices: reach:on} @@ -14944,7 +14944,7 @@ Choices: reach:on} reachDependenciesStoreSimpleEQ { \assumes ([equals(store(h,o3,f2,x),h2)]==>[]) \find(reach(h2,allObjects(f),o,o2,n)) -\varcond(\metaDisjoint f (Field term), f2 (Field term), ) +\varcond(\metaDisjoint f (Field term), f2 (Field term)) \replacewith(reach(h,allObjects(f),o,o2,n)) \heuristics(simplify) Choices: reach:on} @@ -14960,7 +14960,7 @@ Choices: reach:on} reachEndOfUniquePath { \assumes ([reach(h,allObjects(f),o,o2,n),equals(alpha::select(h,o2,f),null),equals(alpha::select(h,o3,f),null)]==>[]) \find(reach(h,allObjects(f),o,o3,n2)==>) -\varcond(\different (n (int term), n2 (int term)), ) +\varcond(\different (n (int term), n2 (int term))) \add [and(equals(o2,o3),equals(n,n2))]==>[] \heuristics(inReachableStateImplication) Choices: reach:on} @@ -14969,7 +14969,7 @@ Choices: reach:on} reachEndOfUniquePath2 { \assumes ([reach(h,allObjects(f),o,o2,n),equals(alpha::select(h,o2,f),null)]==>[]) \find(reach(h,allObjects(f),o,o3,n2)==>) -\varcond(\different (o (java.lang.Object term), o2 (java.lang.Object term)), \different (n (int term), n2 (int term)), ) +\varcond(\different (o (java.lang.Object term), o2 (java.lang.Object term)), \different (n (int term), n2 (int term))) \add [or(lt(n2,n),and(equals(o2,o3),equals(n,n2)))]==>[] \heuristics(inReachableStateImplication) Choices: reach:on} @@ -14999,7 +14999,7 @@ Choices: reach:on} reachUniquePathSameSteps { \assumes ([reach(h,allObjects(f),o,o2,n)]==>[]) \find(reach(h,allObjects(f),o,o3,n)==>) -\varcond(\different (o2 (java.lang.Object term), o3 (java.lang.Object term)), ) +\varcond(\different (o2 (java.lang.Object term), o3 (java.lang.Object term))) \add [equals(o2,o3)]==>[] \heuristics(inReachableStateImplication) Choices: reach:on} @@ -15048,7 +15048,7 @@ reference_type_cast { \find(==>#allmodal ( (modal operator))\[{ .. #lhs = (#npit) #se; ... }\] (post)) -\varcond(\hasSort(#npit (program NonPrimitiveType), G), \not\sub(\typeof(#se (program SimpleExpression)), G), ) +\varcond(\hasSort(#npit (program NonPrimitiveType), G), \not\sub(\typeof(#se (program SimpleExpression)), G)) \add []==>[or(equals(#se,null),equals(G::instance(#se),TRUE))] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(#lhs (program LeftHandSide))(#addCast(#se,#lhs)),#allmodal(post))]) \heuristics(simplify_prog) @@ -15459,7 +15459,7 @@ Choices: true} sameTypeFalse { \assumes ([equals(G::exactInstance(x1),TRUE),equals(H::exactInstance(x2),TRUE)]==>[]) \find(sameType(x1,x2)) -\varcond(\not\same(G, H), ) +\varcond(\not\same(G, H)) \replacewith(false) \heuristics(concrete) Choices: true} @@ -16165,7 +16165,7 @@ Choices: true} == simplifyIfThenElseUpdate1 (simplifyIfThenElse) ========================================= simplifyIfThenElseUpdate1 { \find(if-then-else(phi,update-application(u1,t),update-application(u2,t))) -\varcond(\simplifyIfThenElseUpdate(phi, u1, u2, t, result), ) +\varcond(\simplifyIfThenElseUpdate(phi, u1, u2, t, result)) \replacewith(result) Choices: true} @@ -16173,7 +16173,7 @@ Choices: true} == simplifyIfThenElseUpdate2 (simplifyIfThenElse) ========================================= simplifyIfThenElseUpdate2 { \find(if-then-else(phi,t,update-application(u2,t))) -\varcond(\simplifyIfThenElseUpdate(phi, u1, u2, t, result), ) +\varcond(\simplifyIfThenElseUpdate(phi, u1, u2, t, result)) \replacewith(result) Choices: true} @@ -16181,7 +16181,7 @@ Choices: true} == simplifyIfThenElseUpdate3 (simplifyIfThenElse) ========================================= simplifyIfThenElseUpdate3 { \find(if-then-else(phi,update-application(u1,t),t)) -\varcond(\simplifyIfThenElseUpdate(phi, u1, u2, t, result), ) +\varcond(\simplifyIfThenElseUpdate(phi, u1, u2, t, result)) \replacewith(result) Choices: true} @@ -16189,7 +16189,7 @@ Choices: true} == simplifyIfThenElseUpdate4 (simplifyIfThenElse) ========================================= simplifyIfThenElseUpdate4 { \find(if-then-else(phi,t,t)) -\varcond(\simplifyIfThenElseUpdate(phi, u1, u2, t, result), ) +\varcond(\simplifyIfThenElseUpdate(phi, u1, u2, t, result)) \replacewith(result) Choices: true} @@ -16289,7 +16289,7 @@ Choices: programRules:Java} == simplifyUpdate1 (simplifyUpdate1) ========================================= simplifyUpdate1 { \find(update-application(u,t)) -\varcond(\dropEffectlessElementaries(u (update), t (any term), result (any term)), ) +\varcond(\dropEffectlessElementaries(u (update), t (any term), result (any term))) \replacewith(result) \heuristics(update_elim) Choices: true} @@ -16297,7 +16297,7 @@ Choices: true} == simplifyUpdate2 (simplifyUpdate2) ========================================= simplifyUpdate2 { \find(update-application(u,phi)) -\varcond(\dropEffectlessElementaries(u (update), phi (formula), result (formula)), ) +\varcond(\dropEffectlessElementaries(u (update), phi (formula), result (formula))) \replacewith(result) \heuristics(update_elim) Choices: true} @@ -16305,7 +16305,7 @@ Choices: true} == simplifyUpdate3 (simplifyUpdate3) ========================================= simplifyUpdate3 { \find(update-application(u,u2)) -\varcond(\dropEffectlessElementaries(u (update), u2 (update), result (update)), ) +\varcond(\dropEffectlessElementaries(u (update), u2 (update), result (update))) \replacewith(result) \heuristics(update_elim) Choices: true} @@ -16433,7 +16433,7 @@ Choices: true} == sortsDisjoint1 (sortsDisjoint1) ========================================= sortsDisjoint1 { \find(equals(x,y)) -\varcond(\not\sub(Null, G), \disjointModuloNull(G, H), ) +\varcond(\not\sub(Null, G), \disjointModuloNull(G, H)) \replacewith(false) \heuristics(concrete) Choices: true} @@ -16441,7 +16441,7 @@ Choices: true} == sortsDisjoint2 (sortsDisjoint2) ========================================= sortsDisjoint2 { \find(equals(x,y)) -\varcond(\not\sub(Null, H), \disjointModuloNull(G, H), ) +\varcond(\not\sub(Null, H), \disjointModuloNull(G, H)) \replacewith(false) \heuristics(concrete) Choices: true} @@ -16449,7 +16449,7 @@ Choices: true} == sortsDisjointModuloNull (sortsDisjointModuloNull) ========================================= sortsDisjointModuloNull { \find(equals(x,y)) -\varcond(\strict\sub(Null, G), \strict\sub(Null, H), \disjointModuloNull(G, H), ) +\varcond(\strict\sub(Null, G), \strict\sub(Null, H), \disjointModuloNull(G, H)) \replacewith(and(equals(x,null),equals(y,null))) \heuristics(simplify) Choices: true} @@ -16542,7 +16542,7 @@ staticMethodCall { \find(#allmodal ( (modal operator))\[{ .. #se.#mn(#elist); ... }\] (post)) -\varcond(\staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #elist (program Expression)), ) +\varcond(\staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #elist (program Expression))) \replacewith(#allmodal ( (modal operator))\[{ .. method-call(#se.#mn(#elist)) ... }\] (post)) @@ -16579,7 +16579,7 @@ staticMethodCallWithAssignment { \find(#allmodal ( (modal operator))\[{ .. #lhs = #se.#mn(#elist); ... }\] (post)) -\varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #elist (program Expression)), ) +\varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #elist (program Expression))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs) #v0; method-call(#se.#mn(#elist)) @@ -17112,7 +17112,7 @@ synchronizedBlockEmpty { \find(==>#allmodal ( (modal operator))\[{ .. synchronized(#se) {} ... }\] (post)) -\varcond(\isLocalVariable (#se (program SimpleExpression)), ) +\varcond(\isLocalVariable (#se (program SimpleExpression))) \replacewith([]==>[not(equals(#se,null))]) ; \replacewith([]==>[#allmodal(post)]) \heuristics(simplify_prog_subset, simplify_prog) @@ -17134,7 +17134,7 @@ synchronizedBlockEvalSync { #slist } ... }\] (post)) -\varcond(\new(#loc (program Variable), \typeof(#nsencr (program NonSimpleExpressionNoClassReference))), \isLocalVariable (#nsencr (program NonSimpleExpressionNoClassReference)), ) +\varcond(\new(#loc (program Variable), \typeof(#nsencr (program NonSimpleExpressionNoClassReference))), \isLocalVariable (#nsencr (program NonSimpleExpressionNoClassReference))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nsencr) #loc = #nsencr; synchronized(#loc) { @@ -17242,7 +17242,7 @@ throwUnfoldMore { \find(#allmodal ( (modal operator))\[{ .. throw #se; ... }\] (post)) -\varcond(\new(#v0 (program Variable), \typeof(#se (program SimpleExpression))), \isLocalVariable (#se (program SimpleExpression)), ) +\varcond(\new(#v0 (program Variable), \typeof(#se (program SimpleExpression))), \isLocalVariable (#se (program SimpleExpression))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#se) #v0 = #se; throw #v0; @@ -18290,7 +18290,7 @@ unusedLabel { #lb: #s ... }\] (post)) -\varcond(\not\freeLabelIn (#lb,#s), ) +\varcond(\not\freeLabelIn (#lb,#s)) \replacewith(#allmodal ( (modal operator))\[{ .. #s ... }\] (post)) @@ -18418,7 +18418,7 @@ Choices: programRules:Java} == wellFormedMemsetArrayObject (wellFormedMemsetArrayObject) ========================================= wellFormedMemsetArrayObject { \find(wellFormed(memset(h,arrayRange(ar,lo,up),x))) -\succedentPolarity\varcond(\hasSort(\elemSort(ar (java.lang.Object term)), alpha), ) +\succedentPolarity\varcond(\hasSort(\elemSort(ar (java.lang.Object term)), alpha)) \replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::),TRUE),arrayStoreValid(ar,x))))) \heuristics(simplify_enlarging) Choices: programRules:Java} @@ -18426,7 +18426,7 @@ Choices: programRules:Java} == wellFormedMemsetArrayPrimitive (wellFormedMemsetArrayPrimitive) ========================================= wellFormedMemsetArrayPrimitive { \find(wellFormed(memset(h,arrayRange(ar,lo,up),x))) -\succedentPolarity\varcond(\hasSort(\elemSort(ar (java.lang.Object term)), alpha), \not\sub(beta, java.lang.Object), \not\sub(beta, LocSet), \sub(beta, alpha), ) +\succedentPolarity\varcond(\hasSort(\elemSort(ar (java.lang.Object term)), alpha), \not\sub(beta, java.lang.Object), \not\sub(beta, LocSet), \sub(beta, alpha)) \replacewith(wellFormed(h)) \heuristics(simplify_enlarging) Choices: programRules:Java} @@ -18434,7 +18434,7 @@ Choices: programRules:Java} == wellFormedStoreArray (wellFormedStoreArray) ========================================= wellFormedStoreArray { \find(wellFormed(store(h,o,arr(idx),x))) -\succedentPolarity\varcond(\hasSort(\elemSort(o (java.lang.Object term)), alpha), ) +\succedentPolarity\varcond(\hasSort(\elemSort(o (java.lang.Object term)), alpha)) \replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::),TRUE),arrayStoreValid(o,x))))) \heuristics(simplify_enlarging) Choices: programRules:Java} @@ -18442,7 +18442,7 @@ Choices: programRules:Java} == wellFormedStoreLocSet (wellFormedStoreLocSet) ========================================= wellFormedStoreLocSet { \find(wellFormed(store(h,o,f,x))) -\succedentPolarity\varcond(\fieldType(f (Field term), alpha), \sub(LocSet, alpha), ) +\succedentPolarity\varcond(\fieldType(f (Field term), alpha), \sub(LocSet, alpha)) \replacewith(and(wellFormed(h),createdInHeap(x,h))) \heuristics(simplify_enlarging) Choices: programRules:Java} @@ -18458,7 +18458,7 @@ Choices: programRules:Java} == wellFormedStoreObject (wellFormedStoreObject) ========================================= wellFormedStoreObject { \find(wellFormed(store(h,o,f,x))) -\succedentPolarity\varcond(\fieldType(f (Field term), alpha), ) +\succedentPolarity\varcond(\fieldType(f (Field term), alpha)) \replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::),TRUE),equals(alpha::instance(x),TRUE))))) \heuristics(simplify_enlarging) Choices: programRules:Java} @@ -18467,7 +18467,7 @@ Choices: programRules:Java} wellFormedStoreObjectEQ { \assumes ([equals(store(h,o,f,x),EQ)]==>[]) \find(wellFormed(EQ)) -\sameUpdateLevel\succedentPolarity\varcond(\fieldType(f (Field term), alpha), ) +\sameUpdateLevel\succedentPolarity\varcond(\fieldType(f (Field term), alpha)) \replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::),TRUE),equals(alpha::instance(x),TRUE))))) \heuristics(simplify_enlarging) Choices: programRules:Java} @@ -18475,7 +18475,7 @@ Choices: programRules:Java} == wellFormedStorePrimitive (wellFormedStorePrimitive) ========================================= wellFormedStorePrimitive { \find(wellFormed(store(h,o,f,x))) -\succedentPolarity\varcond(\fieldType(f (Field term), alpha), \not\sub(beta, java.lang.Object), \not\sub(beta, LocSet), \sub(beta, alpha), ) +\succedentPolarity\varcond(\fieldType(f (Field term), alpha), \not\sub(beta, java.lang.Object), \not\sub(beta, LocSet), \sub(beta, alpha)) \replacewith(wellFormed(h)) \heuristics(concrete) Choices: programRules:Java} @@ -18483,7 +18483,7 @@ Choices: programRules:Java} == wellFormedStorePrimitiveArray (wellFormedStorePrimitiveArray) ========================================= wellFormedStorePrimitiveArray { \find(wellFormed(store(h,o,arr(idx),x))) -\succedentPolarity\varcond(\hasSort(\elemSort(o (java.lang.Object term)), alpha), \not\sub(beta, java.lang.Object), \not\sub(beta, LocSet), \sub(beta, alpha), ) +\succedentPolarity\varcond(\hasSort(\elemSort(o (java.lang.Object term)), alpha), \not\sub(beta, java.lang.Object), \not\sub(beta, LocSet), \sub(beta, alpha)) \replacewith(wellFormed(h)) \heuristics(concrete) Choices: programRules:Java} @@ -18492,7 +18492,7 @@ Choices: programRules:Java} wellFormedStorePrimitiveEQ { \assumes ([equals(store(h,o,f,x),EQ)]==>[]) \find(wellFormed(EQ)) -\sameUpdateLevel\succedentPolarity\varcond(\not\sub(beta, java.lang.Object), \not\sub(beta, LocSet), ) +\sameUpdateLevel\succedentPolarity\varcond(\not\sub(beta, java.lang.Object), \not\sub(beta, LocSet)) \replacewith(wellFormed(h)) \heuristics(concrete) Choices: programRules:Java} 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 index 790bfa00423..ffd1c600e7c 100644 --- 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,7 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util; + import java.util.Iterator; +import java.util.function.Function; import java.util.regex.Matcher; import java.util.regex.Pattern; @@ -60,18 +62,21 @@ public static boolean isJMLComment(String comment) { * open element1 sep element2 sep element3 close * * @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 + * @param open the String used to open the list + * @param sep the String separating the different elements + * @param close the String used to close the list + * @param mapper a Function that maps the elements of type S to their String representation * @return the CharSequence in the described format * @param the type of the elements of the iterated collection */ - public static String formatAsList(Iterator it, char open, char sep, char close) { + public static String formatAsList(Iterator it, + CharSequence open, CharSequence sep, CharSequence close, + Function mapper) { final StringBuilder str = new StringBuilder(); str.append(open); var hasNext = it.hasNext(); while (hasNext) { - str.append(it.next()); + str.append(mapper.apply(it.next())); hasNext = it.hasNext(); if (hasNext) { str.append(sep); @@ -80,4 +85,54 @@ public static String formatAsList(Iterator it, char open, char sep, char str.append(close); return str.toString(); } + + /** + * outputs the collection represented by the iterator in the format + * open element1 sep element2 sep element3 close + * + * @param it the Iterator over the collection to be printed + * @param open the String used to open the list + * @param sep the String separating the different elements + * @param close the String used to close the list + * @return the CharSequence in the described format + * @param the type of the elements of the iterated collection + */ + public static String formatAsList(Iterator it, + CharSequence open, CharSequence sep, CharSequence close) { + return formatAsList(it, open, sep, close, Function.identity()); + } + + /** + * outputs the collection represented by the iterator in the format + * open element1 sep element2 sep element3 close + * + * @param it the Iterable to be printed + * @param open the String used to open the list + * @param sep the String separating the different elements + * @param close the String used to close the list + * @param mapper a Function that maps the elements of type S to their String representation + * @return the CharSequence in the described format + * @param the type of the elements of the iterated collection + */ + public static String formatAsList(Iterable it, + CharSequence open, CharSequence sep, CharSequence close, + Function mapper) { + return formatAsList(it.iterator(), open, sep, close, mapper); + } + + /** + * outputs the collection represented by the iterator in the format + * open element1 sep element2 sep element3 close + * + * @param it the Iterable to be printed + * @param open the String used to open the list + * @param sep the String separating the different elements + * @param close the String used to close the list + * @return the CharSequence in the described format + * @param the type of the elements of the iterated collection + */ + public static String formatAsList(Iterable it, + CharSequence open, CharSequence sep, CharSequence close) { + return formatAsList(it, open, sep, close, Function.identity()); + } } 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 index 9d62a9d4c83..d2ce01b4165 100644 --- 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 @@ -224,7 +224,7 @@ public Iterator> iterator() { } public String toString() { - return Strings.formatAsList(iterator(), '[', ',', ']'); + 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 index 2fccdb274ae..083e101b765 100644 --- 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 @@ -328,7 +328,7 @@ public static ImmutableSet fromCollection(@Nullable Collection seq) { @Override public String toString() { - return Strings.formatAsList(iterator(), '{', ',', '}'); + return Strings.formatAsList(iterator(), "{", ",", "}"); } /** represents the empty set for elements of type */ 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 index ff42f494f95..4f2f1fef8e6 100644 --- 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 @@ -147,7 +147,7 @@ public boolean equals(Object o) { @Override public String toString() { - return Strings.formatAsList(iterator(), '[', ',', ']'); + 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 index cbceca8efec..48a8a959109 100644 --- 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 @@ -333,7 +333,7 @@ public Iterator sortedIterator() { public String toString() { - return Strings.formatAsList(iterator(), '[', ',', ']'); + 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 index 578cf56e03d..1672d6c6997 100644 --- 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 @@ -453,7 +453,7 @@ public boolean equals(Object o) { @Override public String toString() { - return Strings.formatAsList(this.iterator(), '[', ',', ']'); + 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 index da645e68a63..e36548d1793 100644 --- a/key.util/src/test/java/org/key_project/util/StringsTest.java +++ b/key.util/src/test/java/org/key_project/util/StringsTest.java @@ -4,7 +4,7 @@ package org.key_project.util; import java.util.Arrays; -import java.util.Iterator; +import java.util.List; import org.junit.jupiter.api.Test; @@ -58,13 +58,16 @@ void isJMLComment() { @Test void formatAsList() { - Iterator it = Arrays.stream(new String[] { "a", "b", "c" }).iterator(); - assertEquals("%a;b;c$", Strings.formatAsList(it, '%', ';', '$')); + List testStrings = Arrays.asList("a", "b", "c"); + assertEquals("%a;b;c$", Strings.formatAsList(testStrings, "%", ";", "$")); - it = Arrays.stream(new String[] { "a" }).iterator(); - assertEquals("%a$", Strings.formatAsList(it, '%', ';', '$')); + assertEquals("%1;1;1$", + Strings.formatAsList(testStrings, "%", ";", "$", String::length)); - it = Arrays.stream(new String[] {}).iterator(); - assertEquals("%$", Strings.formatAsList(it, '%', ';', '$')); + testStrings = Arrays.asList("a"); + assertEquals("%a$", Strings.formatAsList(testStrings, "%", ";", "$")); + + testStrings = Arrays.asList(new String[] {}); + assertEquals("%$", Strings.formatAsList(testStrings, "%", ";", "$")); } } From 64877fed353921192e32cf1406381c7a44b38dc4 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 20 Oct 2023 20:47:38 +0200 Subject: [PATCH 3/4] Add some more test cases for Strings#isJMLComment --- .../src/test/java/org/key_project/util/StringsTest.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 index e36548d1793..d60b5c8a3ff 100644 --- a/key.util/src/test/java/org/key_project/util/StringsTest.java +++ b/key.util/src/test/java/org/key_project/util/StringsTest.java @@ -38,12 +38,14 @@ void isJMLComment() { String[] correctComments = { "/*@ requires ", "//@ requires", "/*+KeY@ requires", "//+KeY@ requires", - "/*-OtherTool@", "//-OtherTool@" + "/*-OtherTool@ requires", "//-OtherTool@ requires" }; String[] inCorrectComments = { "/* @ requires ", "// @ requires", + "/* +KeY@ requires", "//+KeY requires", "/*+OtherTool@ requires", "//+OtherTool@ requires", - "/*-KeY@", "//*-KeY@" + "/*-OtherTool requires", "//-OtherTool requires", + "/*-KeY@ requires", "//*-KeY@ requires" }; for (var comment : correctComments) { From 4b131f4453f91347005ffe25db69aef481322114 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sun, 22 Oct 2023 19:37:27 +0200 Subject: [PATCH 4/4] Simplify string formatting following a suggestion Alexander Weigl --- .../de/uka/ilkd/key/logic/op/Function.java | 2 +- .../java/org/key_project/util/Strings.java | 52 ++----------------- .../util/collection/DefaultImmutableMap.java | 2 +- .../util/collection/DefaultImmutableSet.java | 2 +- .../util/collection/ImmutableArray.java | 2 +- .../util/collection/ImmutableLeftistHeap.java | 2 +- .../util/collection/ImmutableSLList.java | 2 +- 7 files changed, 11 insertions(+), 53 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 index 4e1a5795998..95bf6cd2d63 100644 --- 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 @@ -116,7 +116,7 @@ public final String proofToString() { new StringBuilder((sort() == Sort.FORMULA ? "" : sort().toString()) + " "); s.append(name()); if (arity() > 0) { - s.append(Strings.formatAsList(argSorts().iterator(), "(", ",", ")")); + s.append(Strings.formatAsList(argSorts(), "(", ",", ")")); } 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 index ffd1c600e7c..200cc051283 100644 --- a/key.util/src/main/java/org/key_project/util/Strings.java +++ b/key.util/src/main/java/org/key_project/util/Strings.java @@ -4,10 +4,11 @@ package org.key_project.util; -import java.util.Iterator; import java.util.function.Function; import java.util.regex.Matcher; import java.util.regex.Pattern; +import java.util.stream.Collectors; +import java.util.stream.StreamSupport; /** * Helper functions for {@link String}s @@ -57,51 +58,6 @@ public static boolean isJMLComment(String comment) { } } - /** - * outputs the collection represented by the iterator in the format - * open element1 sep element2 sep element3 close - * - * @param it the Iterator over the collection to be printed - * @param open the String used to open the list - * @param sep the String separating the different elements - * @param close the String used to close the list - * @param mapper a Function that maps the elements of type S to their String representation - * @return the CharSequence in the described format - * @param the type of the elements of the iterated collection - */ - public static String formatAsList(Iterator it, - CharSequence open, CharSequence sep, CharSequence close, - Function mapper) { - final StringBuilder str = new StringBuilder(); - str.append(open); - var hasNext = it.hasNext(); - while (hasNext) { - str.append(mapper.apply(it.next())); - hasNext = it.hasNext(); - if (hasNext) { - str.append(sep); - } - } - str.append(close); - return str.toString(); - } - - /** - * outputs the collection represented by the iterator in the format - * open element1 sep element2 sep element3 close - * - * @param it the Iterator over the collection to be printed - * @param open the String used to open the list - * @param sep the String separating the different elements - * @param close the String used to close the list - * @return the CharSequence in the described format - * @param the type of the elements of the iterated collection - */ - public static String formatAsList(Iterator it, - CharSequence open, CharSequence sep, CharSequence close) { - return formatAsList(it, open, sep, close, Function.identity()); - } - /** * outputs the collection represented by the iterator in the format * open element1 sep element2 sep element3 close @@ -117,7 +73,9 @@ public static String formatAsList(Iterator it, public static String formatAsList(Iterable it, CharSequence open, CharSequence sep, CharSequence close, Function mapper) { - return formatAsList(it.iterator(), open, sep, close, mapper); + return StreamSupport.stream(it.spliterator(), false) + .map(a -> mapper.apply(a).toString()) + .collect(Collectors.joining(sep, open, close)); } /** 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 index d2ce01b4165..b902f17915f 100644 --- 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 @@ -224,7 +224,7 @@ public Iterator> iterator() { } public String toString() { - return Strings.formatAsList(iterator(), "[", ",", "]"); + return Strings.formatAsList(this, "[", ",", "]"); } @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 index 083e101b765..9a5f6f4997d 100644 --- 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 @@ -328,7 +328,7 @@ public static ImmutableSet fromCollection(@Nullable Collection seq) { @Override public String toString() { - return Strings.formatAsList(iterator(), "{", ",", "}"); + return Strings.formatAsList(this, "{", ",", "}"); } /** represents the empty set for elements of type */ 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 index 4f2f1fef8e6..2ea2233e2fd 100644 --- 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 @@ -147,7 +147,7 @@ public boolean equals(Object o) { @Override public String toString() { - return Strings.formatAsList(iterator(), "[", ",", "]"); + return Strings.formatAsList(this, "[", ",", "]"); } @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 index 48a8a959109..9b981683b32 100644 --- 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 @@ -333,7 +333,7 @@ public Iterator sortedIterator() { public String toString() { - return Strings.formatAsList(iterator(), "[", ",", "]"); + return Strings.formatAsList(this, "[", ",", "]"); } 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 index 1672d6c6997..50106229327 100644 --- 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 @@ -453,7 +453,7 @@ public boolean equals(Object o) { @Override public String toString() { - return Strings.formatAsList(this.iterator(), "[", ",", "]"); + return Strings.formatAsList(this, "[", ",", "]"); } }