Show variables by their name, with a line only to tell instances apart

Errors and context refinements wrote every variable instance with its
verifier-wide counter in superscript digits (box¹⁵), which matched nothing
in the code and mixed two Unicode blocks that many fonts draw unevenly.
Each error, and each context refinement, now names its variables in one
scope: a variable written alike to no other keeps its plain name; when
several are, the declared variable or the latest instance shown keeps it
and each other one gets the line its value comes from (x@12), numbered
only when they share a line or have none (x@12#1). The message,
counterexample and Found steps share the error's names, exposed with
getDisplayNames(); ContextHistory.format(refinement) does the same for the
context view. Verification, internal names and the translation table are
unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java

@@ -78,4 +78,11 @@ static int count() {
     int pickByCount() {
         return random.nextInt(count()); // Expect: Refinement Error
     }
+
+    // the earlier values of a variable are written with the line they come from
+    void negate() {
+        @Refinement("_ > 0")
+        int b = 8;
+        b = -b; // Expect: Refinement Error
+    }
 }

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

@@ -15,7 +15,9 @@
 import liquidjava.rj_language.ast.Enum;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Var;
-import liquidjava.rj_language.ast.formatter.VariableFormatter;
+import liquidjava.processor.context.PlacementInCode;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.smt.Counterexample;
 import liquidjava.utils.GeneratedNames;
@@ -41,19 +43,27 @@ public class RefinementError extends LJError {
     private final VCSimplificationResult found;
     private final Counterexample counterexample;
     private final SourcePosition declarationPosition;
+    private final DisplayNames displayNames;
 
     public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
             String customMessage) {
-        super("Refinement Error", message(expected, found), position, translationTable, customMessage);
+        this(position, declarationPosition, expected, found, translationTable, counterexample, customMessage,
+                displayNames(expected, found, translationTable));
+    }
+
+    private RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
+            VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
+            String customMessage, DisplayNames displayNames) {
+        super("Refinement Error", message(expected, found, displayNames), position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
         this.counterexample = filterCounterexample(counterexample);
         this.declarationPosition = declarationPosition;
+        this.displayNames = displayNames;
         if (!this.counterexample.isEmpty()) {
             String counterexampleString = this.counterexample.assignments().stream()
-                    .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
-                    .collect(Collectors.joining(" && "));
+                    .map(a -> displayNames.get(a.first()) + " == " + a.second()).collect(Collectors.joining(" && "));
             setCounterexampleStr("Counterexample: " + counterexampleString);
         }
         setCategory(categoryOf(expected, found));
@@ -64,13 +74,35 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
 
     // Only the facts of found about the values expected constrains; path conditions about other values stay in the
     // derivation
-    private static String message(Predicate expected, VCSimplificationResult found) {
-        Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(),
-                expected.getExpression());
+    private static String message(Predicate expected, VCSimplificationResult found, DisplayNames names) {
+        Expression shown = shownFound(expected, found);
+        String expectedString = ExpressionFormatter.format(expected.getExpression(), names);
         if (isTrue(shown))
-            return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString());
-        return String.format("%s is not a subtype of %s", shown.toDisplayString(),
-                expected.getExpression().toDisplayString());
+            return String.format("expected %s but could not prove it", expectedString);
+        return String.format("%s is not a subtype of %s", ExpressionFormatter.format(shown, names), expectedString);
+    }
+
+    /** The facts of found that the message shows */
+    static Expression shownFound(Predicate expected, VCSimplificationResult found) {
+        return linkedToExpected(found.getImplication().toPredicate().getExpression(), expected.getExpression());
+    }
+
+    /**
+     * The names of an error's variables: those of its message come first, then those only the steps of found show, each
+     * with the line its value comes from
+     */
+    static DisplayNames displayNames(Predicate expected, VCSimplificationResult found,
+            TranslationTable translationTable) {
+        List<String> shown = new ArrayList<>();
+        shownFound(expected, found).getVariableNames(shown);
+        expected.getExpression().getVariableNames(shown);
+        VCSimplificationResult original = original(found);
+        List<String> others = original.getBinders();
+        original.getImplication().toPredicate().getExpression().getVariableNames(others);
+        return DisplayNames.of(shown, others, name -> {
+            PlacementInCode placement = translationTable == null ? null : translationTable.get(name);
+            return placement == null ? null : placement.getLine();
+        });
     }
 
     /** Unknown when what was found says nothing about the values the expected refinement constrains */
@@ -97,6 +129,11 @@ public VCSimplificationResult getFound() {
         return found;
     }
 
+    /** The names this error gives its variables, for every view of it to show them alike */
+    public DisplayNames getDisplayNames() {
+        return displayNames;
+    }
+
     // Keeps the counterexample assignments to the terms of expected and of the found facts linked to them, except
     // values found already states, so there is none when found fixes every value expected depends on. The terms of
     // expected come first, those found says nothing about before the rest, then the linked terms in the order of the
@@ -144,10 +181,14 @@ private static boolean states(Expression term, Expression value, Pair<String, St
 
     // Binders of the VC chain before simplification, which keeps the variables in the order they were introduced
     private List<String> originalBinders() {
-        VCSimplificationResult original = getFound();
+        return original(getFound()).getBinders();
+    }
+
+    private static VCSimplificationResult original(VCSimplificationResult found) {
+        VCSimplificationResult original = found;
         while (original.getOrigin() != null)
             original = original.getOrigin();
-        return original.getBinders();
+        return original;
     }
 
     // 0 for terms of expected found says nothing about, whose values alone break it, 1 for the other terms of

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

@@ -1,7 +1,6 @@
 package liquidjava.diagnostics.errors;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
-import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected;
 
 import java.util.List;
 
@@ -12,6 +11,8 @@
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import spoon.reflect.cu.SourcePosition;
 
@@ -26,11 +27,21 @@ public class StateRefinementError extends LJError {
     private final VCSimplificationResult found;
     private final SourcePosition declarationPosition;
     private final StateErrorContext context;
+    private final DisplayNames displayNames;
 
     public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
             ErrorCategory category, StateErrorContext context) {
-        super("State Refinement Error", message(expected, found), position, translationTable, customMessage);
+        this(position, declarationPosition, expected, found, translationTable, customMessage, hints, category, context,
+                RefinementError.displayNames(expected, found, translationTable));
+    }
+
+    private StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
+            VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
+            ErrorCategory category, StateErrorContext context, DisplayNames displayNames) {
+        super("State Refinement Error", message(expected, found, displayNames), position, translationTable,
+                customMessage);
+        this.displayNames = displayNames;
         this.declarationPosition = declarationPosition;
         this.expected = expected;
         this.found = found;
@@ -44,13 +55,12 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
 
     // Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a
     // guard on another value says nothing about the state expected needs
-    private static String message(Predicate expected, VCSimplificationResult found) {
-        Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(),
-                expected.getExpression());
+    private static String message(Predicate expected, VCSimplificationResult found, DisplayNames names) {
+        Expression shown = RefinementError.shownFound(expected, found);
+        String expectedString = ExpressionFormatter.format(expected.getExpression(), names);
         if (!appliesGhost(shown))
-            return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString());
-        return String.format("found %s but expected %s", shown.toDisplayString(),
-                expected.getExpression().toDisplayString());
+            return String.format("expected %s but could not prove it", expectedString);
+        return String.format("found %s but expected %s", ExpressionFormatter.format(shown, names), expectedString);
     }
 
     private static boolean appliesGhost(Expression expression) {
@@ -75,6 +85,11 @@ public VCSimplificationResult getFoundSimplification() {
         return found;
     }
 
+    /** The names this error gives its variables, for every view of it to show them alike */
+    public DisplayNames getDisplayNames() {
+        return displayNames;
+    }
+
     /** What is known about the receiver's states, or null if they could not be computed */
     public StateErrorContext getContext() {
         return context;

liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java

@@ -4,8 +4,12 @@
 import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
+import java.util.stream.Stream;
 
 import liquidjava.api.CommandLineLauncher;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
@@ -96,4 +100,19 @@ public Set<RefinedFunction> getMethods() {
     public Map<String, Set<String>> getFileScopes() {
         return fileScopes;
     }
+
+    /**
+     * A refinement as the context shows it, its variables named as in {@link DisplayNames} with the lines of the
+     * variables saved here
+     */
+    public String format(Predicate refinement) {
+        DisplayNames names = DisplayNames.of(refinement.getVariableNames(), Set.of(), this::lineOf);
+        return ExpressionFormatter.format(refinement.getExpression(), names);
+    }
+
+    private Integer lineOf(String name) {
+        return Stream.concat(localVars.stream(), globalVars.stream()).filter(v -> v.getName().equals(name))
+                .map(RefinedVariable::getPlacementInCode).filter(p -> p != null).map(PlacementInCode::getLine)
+                .findFirst().orElse(null);
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java

@@ -31,6 +31,11 @@ public SourcePosition getAnnotationPosition() {
         return annotationPosition;
     }
 
+    /** The line of this placement, or null when it is not in code */
+    public Integer getLine() {
+        return position == null || !position.isValidPosition() ? null : position.getLine();
+    }
+
     public static PlacementInCode createPlacement(CtElement elem) {
         CtElement elemCopy = elem.clone();
         // cleanup annotations

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/DisplayNames.java

@@ -0,0 +1,78 @@
+package liquidjava.rj_language.ast.formatter;
+
+import java.util.Collection;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+/**
+ * The names of the variables of one scope, such as an error or a refinement, as they are shown. A name is written as in
+ * code; when the scope has several variables written alike, one keeps the plain name and each other one gets the line
+ * its value comes from, {@code x@12}, numbered when they share a line or have none, {@code x@12#1} and {@code x@12#2}.
+ * The plain name goes to the declared variable, or else to its latest instance, preferring those shown first
+ */
+public final class DisplayNames {
+    private final Map<String, String> tags = new HashMap<>();
+
+    private DisplayNames() {
+    }
+
+    /**
+     * @param shown
+     *            the names shown first, such as those of an error message
+     * @param others
+     *            the other names of the scope
+     * @param lineOf
+     *            the line where the value of a variable comes from, or null when unknown
+     */
+    public static DisplayNames of(Collection<String> shown, Collection<String> others,
+            Function<String, Integer> lineOf) {
+        DisplayNames names = new DisplayNames();
+        Set<String> all = new LinkedHashSet<>(shown);
+        all.addAll(others);
+        Map<String, List<String>> alike = all.stream().collect(Collectors.groupingBy(VariableFormatter::format));
+        for (List<String> variables : alike.values()) {
+            if (variables.size() > 1)
+                names.tag(variables, shown, lineOf);
+        }
+        return names;
+    }
+
+    /**
+     * The names of an expression on its own, which has no lines to tell its variables apart
+     */
+    static DisplayNames of(List<String> names) {
+        return of(names, List.of(), name -> null);
+    }
+
+    /**
+     * The display name of a variable, or of a ghost application over variables such as {@code size(#s_2)}
+     */
+    public String get(String name) {
+        return VariableFormatter.format(name, variable -> tags.getOrDefault(variable, ""));
+    }
+
+    private void tag(List<String> alike, Collection<String> shown, Function<String, Integer> lineOf) {
+        List<String> candidates = alike.stream().filter(shown::contains).toList();
+        String plain = (candidates.isEmpty() ? alike : candidates).stream()
+                .max(Comparator.comparing((String name) -> VariableFormatter.counterOf(name) < 0)
+                        .thenComparing(VariableFormatter::counterOf))
+                .orElseThrow();
+        Map<String, List<String>> byLine = alike.stream().filter(name -> !name.equals(plain))
+                .sorted(Comparator.comparingInt(VariableFormatter::counterOf))
+                .collect(Collectors.groupingBy(name -> lineTag(lineOf.apply(name))));
+        byLine.forEach((line, variables) -> {
+            for (int i = 0; i < variables.size(); i++)
+                tags.put(variables.get(i), variables.size() == 1 && !line.isEmpty() ? line : line + "#" + (i + 1));
+        });
+    }
+
+    private static String lineTag(Integer line) {
+        return line == null ? "" : "@" + line;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java

@@ -1,5 +1,6 @@
 package liquidjava.rj_language.ast.formatter;
 
+import java.util.ArrayList;
 import java.util.List;
 import java.util.stream.Collectors;
 
@@ -28,16 +29,25 @@ public class ExpressionFormatter implements ExpressionVisitor<String> {
 
     private final ExpressionNameResolver nameResolver;
 
-    private ExpressionFormatter(Expression expression) {
-        this.nameResolver = ExpressionNameResolver.forExpression(expression);
+    private ExpressionFormatter(Expression expression, DisplayNames names) {
+        this.nameResolver = ExpressionNameResolver.forExpression(expression, names);
     }
 
     public static String format(Predicate predicate) {
         return format(predicate.getExpression());
     }
 
     public static String format(Expression expression) {
-        return new ExpressionFormatter(expression).formatExpression(expression);
+        List<String> variables = new ArrayList<>();
+        expression.getVariableNames(variables);
+        return format(expression, DisplayNames.of(variables));
+    }
+
+    /**
+     * Formats an expression of a scope, such as an error, naming its variables as the scope does
+     */
+    public static String format(Expression expression, DisplayNames names) {
+        return new ExpressionFormatter(expression, names).formatExpression(expression);
     }
 
     private String formatExpression(Expression expression) {

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java

@@ -13,15 +13,20 @@
 final class ExpressionNameResolver {
     private final Set<String> variables = new HashSet<>();
     private final Set<String> functions = new HashSet<>();
+    private final DisplayNames names;
 
-    public static ExpressionNameResolver forExpression(Expression expression) {
-        ExpressionNameResolver resolver = new ExpressionNameResolver();
+    private ExpressionNameResolver(DisplayNames names) {
+        this.names = names;
+    }
+
+    public static ExpressionNameResolver forExpression(Expression expression, DisplayNames names) {
+        ExpressionNameResolver resolver = new ExpressionNameResolver(names);
         resolver.collect(expression);
         return resolver;
     }
 
     public String resolveVariable(String name) {
-        String formatted = VariableFormatter.format(name);
+        String formatted = names.get(name);
         // a field or call argument is always written as in code, as its binder and the counterexample write it
         if (VariableFormatter.isField(name) || ArgumentDisplayNames.argumentCode(name) != null)
             return formatted;