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/AliasExpansion.java

@@ -11,6 +11,8 @@
 import liquidjava.rj_language.ast.AliasInvocation;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.ast.formatter.DisplayNames;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -40,19 +42,19 @@ public String declaration() {
 
     /**
      * The expansions of the alias invocations in an expression, each invocation once in order of appearance, followed
-     * by those of the aliases their definitions use
+     * by those of the aliases their definitions use, naming the variables as the diagnostic does
      */
-    public static List<AliasExpansion> of(Expression expression, List<AliasWrapper> aliases) {
+    public static List<AliasExpansion> of(Expression expression, List<AliasWrapper> aliases, DisplayNames names) {
         Map<String, AliasWrapper> byName = new LinkedHashMap<>();
         for (AliasWrapper alias : aliases)
             byName.put(alias.getName(), alias);
         Map<String, AliasExpansion> expansions = new LinkedHashMap<>();
-        collect(expression, byName, expansions, new HashSet<>());
+        collect(expression, byName, names, expansions, new HashSet<>());
         return new ArrayList<>(expansions.values());
     }
 
     // Expands the invocations under expression, skipping aliases already being expanded so recursive ones end
-    private static void collect(Expression expression, Map<String, AliasWrapper> aliases,
+    private static void collect(Expression expression, Map<String, AliasWrapper> aliases, DisplayNames names,
             Map<String, AliasExpansion> expansions, Set<String> expanding) {
         List<AliasInvocation> invocations = new ArrayList<>();
         invocationsOf(expression, invocations);
@@ -64,14 +66,16 @@ private static void collect(Expression expression, Map<String, AliasWrapper> ali
             if (alias == null || expanding.contains(alias.getName()) || expansions.containsKey(key))
                 continue;
             Expression body = substituteArguments(alias, invocation.getArgs());
-            expansions.put(key, new AliasExpansion(invocation.toDisplayString(), body.toDisplayString(),
-                    alias.getName(), alias.getVarNames(), alias.getDefinition(), alias.getPosition()));
+            expansions.put(key,
+                    new AliasExpansion(ExpressionFormatter.format(invocation, names),
+                            ExpressionFormatter.format(body, names), alias.getName(), alias.getVarNames(),
+                            alias.getDefinition(), alias.getPosition()));
             bodies.put(key, body);
         }
         for (Map.Entry<String, Expression> body : bodies.entrySet()) {
             Set<String> inner = new HashSet<>(expanding);
             inner.add(expansions.get(body.getKey()).alias());
-            collect(body.getValue(), aliases, expansions, inner);
+            collect(body.getValue(), aliases, names, expansions, inner);
         }
     }
 

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

@@ -19,7 +19,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;
@@ -48,24 +50,32 @@ public class RefinementError extends LJError {
     private final List<AliasExpansion> foundAliases;
     private final List<AliasExpansion> expectedAliases;
     private final List<String> aliasDeclarations;
+    private final DisplayNames displayNames;
 
     public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
             String customMessage, List<AliasWrapper> aliases) {
-        super("Refinement Error", message(expected, found), position, translationTable, customMessage);
+        this(position, declarationPosition, expected, found, translationTable, counterexample, customMessage, aliases,
+                displayNames(expected, found, translationTable));
+    }
+
+    private RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
+            VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
+            String customMessage, List<AliasWrapper> aliases, DisplayNames displayNames) {
+        super("Refinement Error", message(expected, found, displayNames), position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
         Expression foundExpression = found.getImplication().toPredicate().getExpression();
-        this.foundAliases = AliasExpansion.of(foundExpression, aliases);
-        this.expectedAliases = AliasExpansion.of(expected.getExpression(), aliases);
+        this.foundAliases = AliasExpansion.of(foundExpression, aliases, displayNames);
+        this.expectedAliases = AliasExpansion.of(expected.getExpression(), aliases, displayNames);
         this.aliasDeclarations = aliasDeclarations(linkedToExpected(foundExpression, expected.getExpression()),
-                expected.getExpression(), aliases);
+                expected.getExpression(), aliases, displayNames);
         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));
@@ -76,21 +86,43 @@ 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();
+        });
     }
 
     // Each alias the message uses once, with those their definitions use, as declared
     private static List<String> aliasDeclarations(Expression shownFound, Expression expected,
-            List<AliasWrapper> aliases) {
+            List<AliasWrapper> aliases, DisplayNames names) {
         Map<String, String> declarations = new LinkedHashMap<>();
         for (Expression shown : List.of(shownFound, expected))
-            for (AliasExpansion expansion : AliasExpansion.of(shown, aliases))
+            for (AliasExpansion expansion : AliasExpansion.of(shown, aliases, names))
                 declarations.putIfAbsent(expansion.alias(), expansion.declaration());
         return new ArrayList<>(declarations.values());
     }
@@ -135,6 +167,11 @@ public List<String> getMessageNotes() {
         return aliasDeclarations.stream().map(declaration -> "where " + declaration).toList();
     }
 
+    /** 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
@@ -182,10 +219,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