Skip to content

Commit 833c7d3

Browse files
rcosta358rcosta358
authored
Instance Variable Superscript Notation (#189)
1 parent 41d3de4 commit 833c7d3

6 files changed

Lines changed: 126 additions & 19 deletions

File tree

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

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
import liquidjava.diagnostics.TranslationTable;
88
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
99
import liquidjava.smt.Counterexample;
10+
import liquidjava.utils.VariableFormatter;
1011
import spoon.reflect.cu.SourcePosition;
1112

1213
/**
@@ -22,7 +23,9 @@ public class RefinementError extends LJError {
2223

2324
public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
2425
TranslationTable translationTable, Counterexample counterexample, String customMessage) {
25-
super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
26+
super("Refinement Error",
27+
String.format("%s is not a subtype of %s", VariableFormatter.formatText(found.getValue().toString()),
28+
VariableFormatter.formatText(expected.getValue().toString())),
2629
position, translationTable, customMessage);
2730
this.expected = expected;
2831
this.found = found;
@@ -47,7 +50,7 @@ public String getCounterExampleString() {
4750
// only include variables that appear in the found value
4851
.filter(a -> foundVarNames.contains(a.first()))
4952
// format as "var == value"
50-
.map(a -> a.first() + " == " + a.second())
53+
.map(a -> VariableFormatter.formatVariable(a.first()) + " == " + a.second())
5154
// join with "&&"
5255
.collect(Collectors.joining(" && "));
5356

@@ -68,4 +71,4 @@ public ValDerivationNode getExpected() {
6871
public ValDerivationNode getFound() {
6972
return found;
7073
}
71-
}
74+
}

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

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
import liquidjava.diagnostics.TranslationTable;
44
import liquidjava.rj_language.ast.Expression;
5+
import liquidjava.utils.VariableFormatter;
56
import spoon.reflect.cu.SourcePosition;
67

78
/**
@@ -16,11 +17,11 @@ public class StateRefinementError extends LJError {
1617

1718
public StateRefinementError(SourcePosition position, Expression expected, Expression found,
1819
TranslationTable translationTable, String customMessage) {
19-
super("State Refinement Error",
20-
String.format("Expected state %s but found %s", expected.toString(), found.toString()), position,
21-
translationTable, customMessage);
22-
this.expected = expected.toString();
23-
this.found = found.toString();
20+
super("State Refinement Error", String.format("Expected state %s but found %s",
21+
VariableFormatter.formatText(expected.toString()), VariableFormatter.formatText(found.toString())),
22+
position, translationTable, customMessage);
23+
this.expected = VariableFormatter.formatText(expected.toString());
24+
this.found = VariableFormatter.formatText(found.toString());
2425
}
2526

2627
public String getExpected() {

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

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
import liquidjava.rj_language.ast.LiteralLong;
1616
import liquidjava.rj_language.ast.LiteralReal;
1717
import liquidjava.rj_language.ast.Var;
18+
import liquidjava.utils.VariableFormatter;
1819

1920
public class ValDerivationNode extends DerivationNode {
2021

@@ -41,17 +42,17 @@ private static class ExpressionSerializer implements JsonSerializer<Expression>
4142
public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationContext context) {
4243
if (exp == null)
4344
return JsonNull.INSTANCE;
44-
if (exp instanceof LiteralInt)
45-
return new JsonPrimitive(((LiteralInt) exp).getValue());
46-
if (exp instanceof LiteralLong)
47-
return new JsonPrimitive(((LiteralLong) exp).getValue());
48-
if (exp instanceof LiteralReal)
49-
return new JsonPrimitive(((LiteralReal) exp).getValue());
50-
if (exp instanceof LiteralBoolean)
51-
return new JsonPrimitive(exp.isBooleanTrue());
52-
if (exp instanceof Var)
53-
return new JsonPrimitive(((Var) exp).getName());
54-
return new JsonPrimitive(exp.toString());
45+
if (exp instanceof LiteralInt v)
46+
return new JsonPrimitive(v.getValue());
47+
if (exp instanceof LiteralLong v)
48+
return new JsonPrimitive(v.getValue());
49+
if (exp instanceof LiteralReal v)
50+
return new JsonPrimitive(v.getValue());
51+
if (exp instanceof LiteralBoolean v)
52+
return new JsonPrimitive(v.isBooleanTrue());
53+
if (exp instanceof Var v)
54+
return new JsonPrimitive(VariableFormatter.formatVariable(v.getName()));
55+
return new JsonPrimitive(VariableFormatter.formatText(exp.toString()));
5556
}
5657
}
5758
}

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,18 @@
11
package liquidjava.rj_language.opt.derivation_node;
22

3+
import java.lang.reflect.Type;
4+
5+
import com.google.gson.JsonElement;
6+
import com.google.gson.JsonPrimitive;
7+
import com.google.gson.JsonSerializationContext;
8+
import com.google.gson.JsonSerializer;
9+
import com.google.gson.annotations.JsonAdapter;
10+
11+
import liquidjava.utils.VariableFormatter;
12+
313
public class VarDerivationNode extends DerivationNode {
414

15+
@JsonAdapter(VariableNameSerializer.class)
516
private final String var;
617
private final DerivationNode origin;
718

@@ -22,4 +33,11 @@ public String getVar() {
2233
public DerivationNode getOrigin() {
2334
return origin;
2435
}
36+
37+
private static class VariableNameSerializer implements JsonSerializer<String> {
38+
@Override
39+
public JsonElement serialize(String src, Type typeOfSrc, JsonSerializationContext context) {
40+
return new JsonPrimitive(VariableFormatter.formatVariable(src));
41+
}
42+
}
2543
}

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

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
package liquidjava.utils;
2+
3+
import java.util.regex.Matcher;
4+
import java.util.regex.Pattern;
5+
6+
public final class VariableFormatter {
7+
private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$");
8+
private static final Pattern INSTANCE_VAR_TEXT_PATTERN = Pattern.compile("#[^\\s,;:()\\[\\]{}]+_[0-9]+");
9+
private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' };
10+
11+
public static String formatVariable(String name) {
12+
if (name == null)
13+
return null;
14+
15+
Matcher matcher = INSTACE_VAR_PATTERN.matcher(name);
16+
if (!matcher.matches())
17+
return name;
18+
19+
String baseName = matcher.group(1);
20+
String counter = matcher.group(2);
21+
String prefix = isSpecialIdentifier(baseName) ? "#" : "";
22+
return prefix + baseName + toSuperscript(counter);
23+
}
24+
25+
public static String formatText(String text) {
26+
if (text == null)
27+
return null;
28+
29+
Matcher textMatcher = INSTANCE_VAR_TEXT_PATTERN.matcher(text);
30+
StringBuilder sb = new StringBuilder();
31+
while (textMatcher.find()) {
32+
String token = textMatcher.group();
33+
textMatcher.appendReplacement(sb, Matcher.quoteReplacement(formatVariable(token)));
34+
}
35+
textMatcher.appendTail(sb);
36+
return sb.toString();
37+
}
38+
39+
private static String toSuperscript(String number) {
40+
StringBuilder sb = new StringBuilder(number.length());
41+
for (char c : number.toCharArray()) {
42+
int index = c - '0';
43+
if (index < 0 || index >= SUPERSCRIPT_CHARS.length)
44+
return number;
45+
sb.append(SUPERSCRIPT_CHARS[index]);
46+
}
47+
return sb.toString();
48+
}
49+
50+
private static boolean isSpecialIdentifier(String id) {
51+
return id.equals("fresh") || id.equals("ret");
52+
}
53+
}

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

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
package liquidjava.variable_formatter;
2+
3+
import static org.junit.jupiter.api.Assertions.assertEquals;
4+
import static org.junit.jupiter.api.Assertions.assertTrue;
5+
6+
import liquidjava.rj_language.ast.Var;
7+
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
8+
import liquidjava.rj_language.opt.derivation_node.VarDerivationNode;
9+
import liquidjava.utils.VariableFormatter;
10+
11+
import org.junit.jupiter.api.Test;
12+
13+
class VariableFormatterTest {
14+
15+
@Test
16+
void testInstanceVariableDisplayNameFormatting() {
17+
assertEquals("x", VariableFormatter.formatVariable("x"));
18+
assertEquals("x²", VariableFormatter.formatVariable("#x_2"));
19+
assertEquals("#fresh¹²", VariableFormatter.formatVariable("#fresh_12"));
20+
assertEquals("#ret³", VariableFormatter.formatVariable("#ret_3"));
21+
assertEquals("this#Class", VariableFormatter.formatVariable("this#Class"));
22+
}
23+
24+
@Test
25+
void testDerivationNodeUsesSuperscriptNotation() {
26+
ValDerivationNode node = new ValDerivationNode(new Var("#x_2"), new VarDerivationNode("#x_2"));
27+
String serialized = node.toString();
28+
assertTrue(serialized.contains("\"value\": \"x²\""), "Expected derivation value to use superscript notation");
29+
assertTrue(serialized.contains("\"var\": \"x²\""), "Expected derivation origin to use superscript notation");
30+
}
31+
}

0 commit comments

Comments
 (0)