Skip to content

Commit 0c1b480

Browse files
rcosta358rcosta358
committed
Refactoring
1 parent ae1c585 commit 0c1b480

File tree

6 files changed

+24
-24
lines changed

6 files changed

+24
-24
lines changed

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +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.VariableNameFormatter;
10+
import liquidjava.utils.VariableFormatter;
1111
import spoon.reflect.cu.SourcePosition;
1212

1313
/**
@@ -24,9 +24,8 @@ public class RefinementError extends LJError {
2424
public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
2525
TranslationTable translationTable, Counterexample counterexample, String customMessage) {
2626
super("Refinement Error",
27-
String.format("%s is not a subtype of %s",
28-
VariableNameFormatter.formatText(found.getValue().toString()),
29-
VariableNameFormatter.formatText(expected.getValue().toString())),
27+
String.format("%s is not a subtype of %s", VariableFormatter.formatText(found.getValue().toString()),
28+
VariableFormatter.formatText(expected.getValue().toString())),
3029
position, translationTable, customMessage);
3130
this.expected = expected;
3231
this.found = found;
@@ -51,7 +50,7 @@ public String getCounterExampleString() {
5150
// only include variables that appear in the found value
5251
.filter(a -> foundVarNames.contains(a.first()))
5352
// format as "var == value"
54-
.map(a -> VariableNameFormatter.formatVariable(a.first()) + " == " + a.second())
53+
.map(a -> VariableFormatter.formatVariable(a.first()) + " == " + a.second())
5554
// join with "&&"
5655
.collect(Collectors.joining(" && "));
5756

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

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

33
import liquidjava.diagnostics.TranslationTable;
44
import liquidjava.rj_language.ast.Expression;
5-
import liquidjava.utils.VariableNameFormatter;
5+
import liquidjava.utils.VariableFormatter;
66
import spoon.reflect.cu.SourcePosition;
77

88
/**
@@ -17,12 +17,11 @@ public class StateRefinementError extends LJError {
1717

1818
public StateRefinementError(SourcePosition position, Expression expected, Expression found,
1919
TranslationTable translationTable, String customMessage) {
20-
super("State Refinement Error",
21-
String.format("Expected state %s but found %s", VariableNameFormatter.formatText(expected.toString()),
22-
VariableNameFormatter.formatText(found.toString())),
20+
super("State Refinement Error", String.format("Expected state %s but found %s",
21+
VariableFormatter.formatText(expected.toString()), VariableFormatter.formatText(found.toString())),
2322
position, translationTable, customMessage);
24-
this.expected = VariableNameFormatter.formatText(expected.toString());
25-
this.found = VariableNameFormatter.formatText(found.toString());
23+
this.expected = VariableFormatter.formatText(expected.toString());
24+
this.found = VariableFormatter.formatText(found.toString());
2625
}
2726

2827
public String getExpected() {

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +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.VariableNameFormatter;
18+
import liquidjava.utils.VariableFormatter;
1919

2020
public class ValDerivationNode extends DerivationNode {
2121

@@ -51,8 +51,8 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo
5151
if (exp instanceof LiteralBoolean v)
5252
return new JsonPrimitive(v.isBooleanTrue());
5353
if (exp instanceof Var v)
54-
return new JsonPrimitive(VariableNameFormatter.formatVariable(v.getName()));
55-
return new JsonPrimitive(VariableNameFormatter.formatText(exp.toString()));
54+
return new JsonPrimitive(VariableFormatter.formatVariable(v.getName()));
55+
return new JsonPrimitive(VariableFormatter.formatText(exp.toString()));
5656
}
5757
}
5858
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
import com.google.gson.JsonSerializer;
99
import com.google.gson.annotations.JsonAdapter;
1010

11-
import liquidjava.utils.VariableNameFormatter;
11+
import liquidjava.utils.VariableFormatter;
1212

1313
public class VarDerivationNode extends DerivationNode {
1414

@@ -37,7 +37,7 @@ public DerivationNode getOrigin() {
3737
private static class VariableNameSerializer implements JsonSerializer<String> {
3838
@Override
3939
public JsonElement serialize(String src, Type typeOfSrc, JsonSerializationContext context) {
40-
return new JsonPrimitive(VariableNameFormatter.formatVariable(src));
40+
return new JsonPrimitive(VariableFormatter.formatVariable(src));
4141
}
4242
}
4343
}

liquidjava-verifier/src/main/java/liquidjava/utils/VariableNameFormatter.java renamed to liquidjava-verifier/src/main/java/liquidjava/utils/VariableFormatter.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
import java.util.regex.Matcher;
55
import java.util.regex.Pattern;
66

7-
public final class VariableNameFormatter {
7+
public final class VariableFormatter {
88
private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$");
99
private static final Pattern INSTANCE_VAR_TEXT_PATTERN = Pattern.compile("#[^\\s,;:()\\[\\]{}]+_[0-9]+");
1010
private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' };

liquidjava-verifier/src/test/java/liquidjava/utils/VariableNameFormatterTest.java renamed to liquidjava-verifier/src/test/java/liquidjava/variable_formatter/VariableFormatterTest.java

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,24 @@
1-
package liquidjava.utils;
1+
package liquidjava.variable_formatter;
22

33
import static org.junit.jupiter.api.Assertions.assertEquals;
44
import static org.junit.jupiter.api.Assertions.assertTrue;
55

66
import liquidjava.rj_language.ast.Var;
77
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
88
import liquidjava.rj_language.opt.derivation_node.VarDerivationNode;
9+
import liquidjava.utils.VariableFormatter;
10+
911
import org.junit.jupiter.api.Test;
1012

11-
class VariableNameFormatterTest {
13+
class VariableFormatterTest {
1214

1315
@Test
1416
void testInstanceVariableDisplayNameFormatting() {
15-
assertEquals("x", VariableNameFormatter.formatVariable("x"));
16-
assertEquals("x²", VariableNameFormatter.formatVariable("#x_2"));
17-
assertEquals("#fresh¹²", VariableNameFormatter.formatVariable("#fresh_12"));
18-
assertEquals("#ret³", VariableNameFormatter.formatVariable("#ret_3"));
19-
assertEquals("this#Class", VariableNameFormatter.formatVariable("this#Class"));
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"));
2022
}
2123

2224
@Test

0 commit comments

Comments
 (0)