Add Similar Name Hint to Not Found Error

liquidjava-verifier/pom.xml

@@ -256,6 +256,7 @@
 		<!-- versions -->
 		<version.junit>5.10.0</version.junit>
 		<version.memcompiler>1.3.0</version.memcompiler>
+		<version.commons-text>1.12.0</version.commons-text>
 		<version.spoon>10.4.2</version.spoon>
 		<version.z3>4.8.17</version.z3>
 		<!-- plugin versions -->
@@ -280,6 +281,11 @@
 		</repository>
 	</repositories>
 	<dependencies>
+		<dependency>
+			<groupId>org.apache.commons</groupId>
+			<artifactId>commons-text</artifactId>
+			<version>${version.commons-text}</version>
+		</dependency>
 		<!-- Only needed to run tests in a version of IntelliJ IDEA that bundles older versions -->
 		<dependency>
 			<groupId>org.junit.platform</groupId>

liquidjava-verifier/src/main/java/liquidjava/diagnostics/NameSuggester.java

@@ -0,0 +1,54 @@
+package liquidjava.diagnostics;
+
+import java.util.Collection;
+import java.util.Comparator;
+import java.util.Locale;
+import java.util.Optional;
+
+import org.apache.commons.text.similarity.JaroWinklerSimilarity;
+
+import liquidjava.utils.Utils;
+
+/**
+ * Finds the closest matching name among the elements available in the current context using Jaro-Winkler similarity
+ */
+public final class NameSuggester {
+
+    private static final int MINIMUM_NAME_LENGTH = 3;
+    private static final double MINIMUM_SIMILARITY = 0.9;
+    private static final JaroWinklerSimilarity SIMILARITY = new JaroWinklerSimilarity();
+
+    private NameSuggester() {
+    }
+
+    public static Optional<String> findClosest(String name, Collection<String> candidates) {
+        if (name == null || candidates == null || candidates.isEmpty())
+            return Optional.empty();
+
+        String sourceName = getSourceName(name);
+        if (sourceName.length() < MINIMUM_NAME_LENGTH)
+            return Optional.empty(); // do not provide suggestions for very short names
+
+        String normalizedSourceName = sourceName.toLowerCase(Locale.ROOT);
+        return candidates.stream().filter(candidate -> candidate != null).map(NameSuggester::getSourceName).distinct()
+                .filter(candidate -> candidate.length() >= MINIMUM_NAME_LENGTH && !candidate.equals(sourceName))
+                .map(candidate -> new Match(candidate,
+                        SIMILARITY.apply(normalizedSourceName, candidate.toLowerCase(Locale.ROOT))))
+                .filter(match -> match.similarity() >= MINIMUM_SIMILARITY)
+                .max(Comparator.comparingDouble(Match::similarity).thenComparing(Match::name,
+                        String.CASE_INSENSITIVE_ORDER.reversed()))
+                .map(Match::name);
+    }
+
+    private static String getSourceName(String name) {
+        String simpleName = Utils.getSimpleName(name);
+        if (simpleName.startsWith("this#"))
+            return simpleName.substring("this#".length());
+        if (simpleName.startsWith("#"))
+            return simpleName.substring(1).replaceFirst("_\\d+$", "");
+        return simpleName;
+    }
+
+    private record Match(String name, double similarity) {
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java

@@ -1,5 +1,9 @@
 package liquidjava.diagnostics.errors;
 
+import java.util.Collection;
+import java.util.Locale;
+
+import liquidjava.diagnostics.NameSuggester;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
@@ -12,27 +16,40 @@
 public class NotFoundError extends LJError {
 
     private final String name;
-    private final String kind; // "Variable" | "Ghost" | "Alias"
+    private final Kind kind;
 
-    public NotFoundError(String name, String kind) {
-        this(null, name, kind, null);
+    public NotFoundError(String name, Kind kind, Collection<String> availableElements) {
+        this(null, name, kind, null, availableElements);
     }
 
-    public NotFoundError(SourcePosition position, String name, String kind) {
-        this(position, name, kind, null);
+    public NotFoundError(SourcePosition position, String name, Kind kind, Collection<String> availableElements) {
+        this(position, name, kind, null, availableElements);
     }
 
-    public NotFoundError(SourcePosition position, String name, String kind, TranslationTable translationTable) {
-        super("Not Found Error", String.format("%s '%s' not found", kind, name), position, translationTable);
+    public NotFoundError(SourcePosition position, String name, Kind kind, TranslationTable translationTable,
+            Collection<String> availableElements) {
+        super("Not Found Error", String.format("%s '%s' could not be found", kind, name), position, translationTable);
         this.name = Utils.getSimpleName(name);
         this.kind = kind;
+        NameSuggester.findClosest(name, availableElements)
+                .ifPresent(match -> setHint(String.format("Did you mean '%s'?", match)));
     }
 
     public String getName() {
         return name;
     }
 
-    public String getKind() {
+    public Kind getKind() {
         return kind;
     }
+
+    public enum Kind {
+        VARIABLE, GHOST, ALIAS, CONSTANT;
+
+        @Override
+        public String toString() {
+            String name = name().toLowerCase(Locale.ROOT);
+            return Character.toUpperCase(name.charAt(0)) + name.substring(1);
+        }
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -206,9 +206,9 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
      */
     private static Predicate createStatePredicate(String value, String targetClass, TypeChecker tc, CtElement e,
             boolean isTo, String prefix) throws LJError {
+        SourcePosition position = Utils.getLJAnnotationPosition(e, value);
         Predicate p = new Predicate(value, e, prefix);
         if (!p.getExpression().isBooleanExpression()) {
-            SourcePosition position = Utils.getLJAnnotationPosition(e, value);
             throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
                     value);
         }
@@ -233,11 +233,9 @@ private static Predicate createStatePredicate(String value, String targetClass,
         Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p;
         Predicate c = c1.substituteVariable(Keys.THIS, name);
         c = c.changeOldMentions(nameOld, name);
-        boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition(), true);
-        if (ok) {
-            SourcePosition pos = Utils.getLJAnnotationPosition(e, value);
-            tc.throwStateConflictError(pos, p);
-        }
+        boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), position, true);
+        if (ok)
+            tc.throwStateConflictError(position, p);
         return c1;
     }
 

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -8,6 +8,7 @@
 
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
+import liquidjava.diagnostics.errors.NotFoundError.Kind;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
@@ -100,7 +101,7 @@ private static Expression resolveStaticFinalConstants(Expression root, CtElement
             String hint = suggested != null ? "Add: import " + suggested + ";"
                     : "Add an import for '" + en.getTypeName() + "' if it is a Java class with a static final field";
             String name = en.getTypeName() + "." + en.getConstName();
-            NotFoundError error = new NotFoundError(pos, name, "Constant");
+            NotFoundError error = new NotFoundError(pos, name, Kind.CONSTANT, List.of());
             error.setHint(hint);
             throw error;
         }

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java

@@ -8,14 +8,14 @@
 import liquidjava.diagnostics.errors.ArgumentMismatchError;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
+import liquidjava.diagnostics.errors.NotFoundError.Kind;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import liquidjava.rj_language.ast.typing.TypeInfer;
 import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.utils.Utils;
-import liquidjava.utils.constants.Keys;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -199,34 +199,33 @@ private void auxSubstituteState(Map<String, Expression> subMap, String[] toChang
     public Expression changeAlias(Map<String, AliasDTO> alias, Context ctx, Factory f) throws LJError {
         Expression e = clone();
         if (this instanceof AliasInvocation ai) {
-            if (alias.containsKey(ai.name)) { // object state
-                AliasDTO dto = alias.get(ai.name);
-                // check argument count
-                if (children.size() != dto.getVarNames().size()) {
+            if (!alias.containsKey(ai.name))
+                throw new NotFoundError(ai.getName(), Kind.ALIAS, alias.keySet());
+            AliasDTO dto = alias.get(ai.name);
+            // check argument count
+            if (children.size() != dto.getVarNames().size()) {
+                String msg = String.format("Wrong number of arguments in alias invocation '%s': expected %d, got %d",
+                        ai.name, dto.getVarNames().size(), children.size());
+                throw new ArgumentMismatchError(msg);
+            }
+            Expression sub = dto.getExpression().clone();
+            for (int i = 0; i < children.size(); i++) {
+                Expression varExp = new Var(dto.getVarNames().get(i));
+                String varType = dto.getVarTypes().get(i);
+                Expression aliasExp = children.get(i);
+
+                // check argument types
+                boolean compatible = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f);
+                if (!compatible) {
                     String msg = String.format(
-                            "Wrong number of arguments in alias invocation '%s': expected %d, got %d", ai.name,
-                            dto.getVarNames().size(), children.size());
+                            "Argument '%s' and parameter '%s' of alias '%s' types are incompatible: expected %s, got %s",
+                            aliasExp, dto.getVarNames().get(i), ai.name, varType,
+                            TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName());
                     throw new ArgumentMismatchError(msg);
                 }
-                Expression sub = dto.getExpression().clone();
-                for (int i = 0; i < children.size(); i++) {
-                    Expression varExp = new Var(dto.getVarNames().get(i));
-                    String varType = dto.getVarTypes().get(i);
-                    Expression aliasExp = children.get(i);
-
-                    // check argument types
-                    boolean compatible = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f);
-                    if (!compatible) {
-                        String msg = String.format(
-                                "Argument '%s' and parameter '%s' of alias '%s' types are incompatible: expected %s, got %s",
-                                aliasExp, dto.getVarNames().get(i), ai.name, varType,
-                                TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName());
-                        throw new ArgumentMismatchError(msg);
-                    }
-                    sub = sub.substitute(varExp, aliasExp);
-                }
-                e = sub;
+                sub = sub.substitute(varExp, aliasExp);
             }
+            e = sub;
         }
         e.auxChangeAlias(alias, ctx, f);
         return e;
@@ -237,7 +236,7 @@ private void auxChangeAlias(Map<String, AliasDTO> alias, Context ctx, Factory f)
             for (int i = 0; i < children.size(); i++) {
                 if (children.get(i)instanceof AliasInvocation ai) {
                     if (!alias.containsKey(ai.name))
-                        throw new NotFoundError(ai.getName(), Keys.ALIAS);
+                        throw new NotFoundError(ai.getName(), Kind.ALIAS, alias.keySet());
                     AliasDTO dto = alias.get(ai.name);
                     // check argument count
                     if (ai.children.size() != dto.getVarNames().size()) {

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -23,11 +23,11 @@
 
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
+import liquidjava.diagnostics.errors.NotFoundError.Kind;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.utils.Pair;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
-import liquidjava.utils.constants.Keys;
 import com.microsoft.z3.enumerations.Z3_sort_kind;
 
 import org.apache.commons.lang3.NotImplementedException;
@@ -120,12 +120,12 @@ public Expr<?> makeBooleanLiteral(boolean value) {
 
     private Expr<?> getVariableTranslation(String name) throws LJError {
         if (!varTranslation.containsKey(name))
-            throw new NotFoundError(name, Keys.VARIABLE);
+            throw new NotFoundError(name, Kind.VARIABLE, varTranslation.keySet());
         Expr<?> e = varTranslation.get(name);
         if (e == null)
             e = varTranslation.get(String.format("this#%s", name));
         if (e == null)
-            throw new NotFoundError(name, Keys.VARIABLE);
+            throw new NotFoundError(name, Kind.VARIABLE, varTranslation.keySet());
         return e;
     }
 
@@ -213,7 +213,7 @@ private FuncDecl<?> resolveFunctionDecl(String name, Expr<?>[] params) throws LJ
         if (candidate != null) {
             return candidate;
         }
-        throw new NotFoundError(name, Keys.GHOST);
+        throw new NotFoundError(name, Kind.GHOST, funcTranslation.keySet());
     }
 
     @SuppressWarnings({ "unchecked", "rawtypes" })

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestNameSuggester.java

@@ -0,0 +1,78 @@
+package liquidjava.api.tests;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import java.util.Arrays;
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.diagnostics.NameSuggester;
+
+class TestNameSuggester {
+
+    @Test
+    void findsClosestName() {
+        assertEquals("amount", NameSuggester.findClosest("ammount", List.of("total", "amount")).orElseThrow());
+    }
+
+    @Test
+    void recognizesTransposedCharacters() {
+        assertEquals("length", NameSuggester.findClosest("lenght", List.of("length")).orElseThrow());
+    }
+
+    @Test
+    void normalizesQualifiedAndGeneratedNames() {
+        assertEquals("length", NameSuggester.findClosest("Example.lenght", List.of("Example.length")).orElseThrow());
+        assertEquals("amount", NameSuggester.findClosest("ammount", List.of("#amount_12")).orElseThrow());
+        assertEquals("value", NameSuggester.findClosest("valuee", List.of("this#value")).orElseThrow());
+    }
+
+    @Test
+    void doesNotSuggestUnrelatedOrVeryShortNames() {
+        assertTrue(NameSuggester.findClosest("counter", List.of("result", "value")).isEmpty());
+        assertTrue(NameSuggester.findClosest("x", List.of("y")).isEmpty());
+    }
+
+    @Test
+    void handlesMissingAndEmptyInputs() {
+        assertTrue(NameSuggester.findClosest(null, List.of("value")).isEmpty());
+        assertTrue(NameSuggester.findClosest("value", null).isEmpty());
+        assertTrue(NameSuggester.findClosest("value", List.of()).isEmpty());
+        assertTrue(NameSuggester.findClosest("", List.of("value")).isEmpty());
+    }
+
+    @Test
+    void ignoresNullBlankAndExactCandidates() {
+        assertEquals("amount", NameSuggester.findClosest("ammount", Arrays.asList(null, "", "amount")).orElseThrow());
+        assertTrue(NameSuggester.findClosest("amount", List.of("amount")).isEmpty());
+        assertTrue(NameSuggester.findClosest("amount", List.of("Example.amount", "#amount_1")).isEmpty());
+    }
+
+    @Test
+    void preservesCandidateCapitalization() {
+        assertEquals("Amount", NameSuggester.findClosest("amount", List.of("Amount")).orElseThrow());
+    }
+
+    @Test
+    void supportsNamesAtMinimumLength() {
+        assertEquals("size", NameSuggester.findClosest("siz", List.of("size")).orElseThrow());
+    }
+
+    @Test
+    void rejectsNamesJustBelowSimilarityThreshold() {
+        assertTrue(NameSuggester.findClosest("abc", List.of("abd")).isEmpty());
+    }
+
+    @Test
+    void prefersTheMostSimilarCandidate() {
+        assertEquals("availableValue",
+                NameSuggester.findClosest("availableValu", List.of("availableValues", "availableValue")).orElseThrow());
+    }
+
+    @Test
+    void breaksEquivalentMatchesAlphabetically() {
+        assertEquals("foobart", NameSuggester.findClosest("foobaru", List.of("foobarv", "foobart")).orElseThrow());
+    }
+}