Instance Variable Superscript Notation

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

@@ -7,6 +7,7 @@
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.smt.Counterexample;
+import liquidjava.utils.VariableFormatter;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -22,7 +23,9 @@ public class RefinementError extends LJError {
 
     public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
             TranslationTable translationTable, Counterexample counterexample, String customMessage) {
-        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
+        super("Refinement Error",
+                String.format("%s is not a subtype of %s", VariableFormatter.formatText(found.getValue().toString()),
+                        VariableFormatter.formatText(expected.getValue().toString())),
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
@@ -47,7 +50,7 @@ public String getCounterExampleString() {
                 // only include variables that appear in the found value
                 .filter(a -> foundVarNames.contains(a.first()))
                 // format as "var == value"
-                .map(a -> a.first() + " == " + a.second())
+                .map(a -> VariableFormatter.formatVariable(a.first()) + " == " + a.second())
                 // join with "&&"
                 .collect(Collectors.joining(" && "));
 
@@ -68,4 +71,4 @@ public ValDerivationNode getExpected() {
     public ValDerivationNode getFound() {
         return found;
     }
-}
+}

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

@@ -2,6 +2,7 @@
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.utils.VariableFormatter;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -16,11 +17,11 @@ public class StateRefinementError extends LJError {
 
     public StateRefinementError(SourcePosition position, Expression expected, Expression found,
             TranslationTable translationTable, String customMessage) {
-        super("State Refinement Error",
-                String.format("Expected state %s but found %s", expected.toString(), found.toString()), position,
-                translationTable, customMessage);
-        this.expected = expected.toString();
-        this.found = found.toString();
+        super("State Refinement Error", String.format("Expected state %s but found %s",
+                VariableFormatter.formatText(expected.toString()), VariableFormatter.formatText(found.toString())),
+                position, translationTable, customMessage);
+        this.expected = VariableFormatter.formatText(expected.toString());
+        this.found = VariableFormatter.formatText(found.toString());
     }
 
     public String getExpected() {

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java

@@ -15,6 +15,7 @@
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.Var;
+import liquidjava.utils.VariableFormatter;
 
 public class ValDerivationNode extends DerivationNode {
 
@@ -41,17 +42,17 @@ private static class ExpressionSerializer implements JsonSerializer<Expression>
         public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationContext context) {
             if (exp == null)
                 return JsonNull.INSTANCE;
-            if (exp instanceof LiteralInt)
-                return new JsonPrimitive(((LiteralInt) exp).getValue());
-            if (exp instanceof LiteralLong)
-                return new JsonPrimitive(((LiteralLong) exp).getValue());
-            if (exp instanceof LiteralReal)
-                return new JsonPrimitive(((LiteralReal) exp).getValue());
-            if (exp instanceof LiteralBoolean)
-                return new JsonPrimitive(exp.isBooleanTrue());
-            if (exp instanceof Var)
-                return new JsonPrimitive(((Var) exp).getName());
-            return new JsonPrimitive(exp.toString());
+            if (exp instanceof LiteralInt v)
+                return new JsonPrimitive(v.getValue());
+            if (exp instanceof LiteralLong v)
+                return new JsonPrimitive(v.getValue());
+            if (exp instanceof LiteralReal v)
+                return new JsonPrimitive(v.getValue());
+            if (exp instanceof LiteralBoolean v)
+                return new JsonPrimitive(v.isBooleanTrue());
+            if (exp instanceof Var v)
+                return new JsonPrimitive(VariableFormatter.formatVariable(v.getName()));
+            return new JsonPrimitive(VariableFormatter.formatText(exp.toString()));
         }
     }
 }

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java

@@ -1,7 +1,18 @@
 package liquidjava.rj_language.opt.derivation_node;
 
+import java.lang.reflect.Type;
+
+import com.google.gson.JsonElement;
+import com.google.gson.JsonPrimitive;
+import com.google.gson.JsonSerializationContext;
+import com.google.gson.JsonSerializer;
+import com.google.gson.annotations.JsonAdapter;
+
+import liquidjava.utils.VariableFormatter;
+
 public class VarDerivationNode extends DerivationNode {
 
+    @JsonAdapter(VariableNameSerializer.class)
     private final String var;
     private final DerivationNode origin;
 
@@ -22,4 +33,11 @@ public String getVar() {
     public DerivationNode getOrigin() {
         return origin;
     }
+
+    private static class VariableNameSerializer implements JsonSerializer<String> {
+        @Override
+        public JsonElement serialize(String src, Type typeOfSrc, JsonSerializationContext context) {
+            return new JsonPrimitive(VariableFormatter.formatVariable(src));
+        }
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java

@@ -0,0 +1,53 @@
+package liquidjava.utils;
+
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+public final class VariableFormatter {
+    private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$");
+    private static final Pattern INSTANCE_VAR_TEXT_PATTERN = Pattern.compile("#[^\\s,;:()\\[\\]{}]+_[0-9]+");
+    private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' };
+
+    public static String formatVariable(String name) {
+        if (name == null)
+            return null;
+
+        Matcher matcher = INSTACE_VAR_PATTERN.matcher(name);
+        if (!matcher.matches())
+            return name;
+
+        String baseName = matcher.group(1);
+        String counter = matcher.group(2);
+        String prefix = isSpecialIdentifier(baseName) ? "#" : "";
+        return prefix + baseName + toSuperscript(counter);
+    }
+
+    public static String formatText(String text) {
+        if (text == null)
+            return null;
+
+        Matcher textMatcher = INSTANCE_VAR_TEXT_PATTERN.matcher(text);
+        StringBuilder sb = new StringBuilder();
+        while (textMatcher.find()) {
+            String token = textMatcher.group();
+            textMatcher.appendReplacement(sb, Matcher.quoteReplacement(formatVariable(token)));
+        }
+        textMatcher.appendTail(sb);
+        return sb.toString();
+    }
+
+    private static String toSuperscript(String number) {
+        StringBuilder sb = new StringBuilder(number.length());
+        for (char c : number.toCharArray()) {
+            int index = c - '0';
+            if (index < 0 || index >= SUPERSCRIPT_CHARS.length)
+                return number;
+            sb.append(SUPERSCRIPT_CHARS[index]);
+        }
+        return sb.toString();
+    }
+
+    private static boolean isSpecialIdentifier(String id) {
+        return id.equals("fresh") || id.equals("ret");
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java

@@ -0,0 +1,31 @@
+package liquidjava.variable_formatter;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+import liquidjava.rj_language.opt.derivation_node.VarDerivationNode;
+import liquidjava.utils.VariableFormatter;
+
+import org.junit.jupiter.api.Test;
+
+class VariableFormatterTest {
+
+    @Test
+    void testInstanceVariableDisplayNameFormatting() {
+        assertEquals("x", VariableFormatter.formatVariable("x"));
+        assertEquals("x²", VariableFormatter.formatVariable("#x_2"));
+        assertEquals("#fresh¹²", VariableFormatter.formatVariable("#fresh_12"));
+        assertEquals("#ret³", VariableFormatter.formatVariable("#ret_3"));
+        assertEquals("this#Class", VariableFormatter.formatVariable("this#Class"));
+    }
+
+    @Test
+    void testDerivationNodeUsesSuperscriptNotation() {
+        ValDerivationNode node = new ValDerivationNode(new Var("#x_2"), new VarDerivationNode("#x_2"));
+        String serialized = node.toString();
+        assertTrue(serialized.contains("\"value\": \"x²\""), "Expected derivation value to use superscript notation");
+        assertTrue(serialized.contains("\"var\": \"x²\""), "Expected derivation origin to use superscript notation");
+    }
+}