From 12bacdcf9a5be0bc8ad42bc7c32e4c541eaffb9c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 14 Jul 2026 19:48:25 +0100 Subject: [PATCH 1/6] Filter & Sort Counterexamples by Binders --- .../diagnostics/errors/RefinementError.java | 37 +++++++------------ .../opt/VCSimplificationResult.java | 14 +++++++ 2 files changed, 28 insertions(+), 23 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index d9297702..a3a6c940 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -6,7 +6,6 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; @@ -45,38 +44,30 @@ public SourcePosition getDeclarationPosition() { @Override public String getDetails() { - String counterexampleString = getCounterExampleString(); - if (counterexampleString == null) + Counterexample counterexamples = getCounterExamples(); + if (counterexamples == null) return ""; + + String counterexampleString = counterexamples.assignments().stream() + .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) + .collect(Collectors.joining(" && ")); return "Counterexample: " + counterexampleString; } - public String getCounterExampleString() { + // Filters counterexample assignments only in found VC and sorts them in the order of its binders + public Counterexample getCounterExamples() { if (counterexample == null || counterexample.assignments().isEmpty()) return null; - List foundVarNames = new ArrayList<>(); - Expression foundExpression = getFound().getImplication().toPredicate().getExpression(); - Expression expectedExpression = expected.getExpression(); - foundExpression.getVariableNames(foundVarNames); - // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the - // subtyping check, so the counterexample maps the symbolic name back to its compile-time value - foundExpression.getResolvedConstantNames(foundVarNames); - expectedExpression.getResolvedConstantNames(foundVarNames); - List foundAssignments = foundExpression.getConjuncts().stream().map(Expression::toString).toList(); - String counterexampleString = counterexample.assignments().stream() - // only include variables that appear in the found value and are not already fixed there - .filter(a -> foundVarNames.contains(a.first()) - && !foundAssignments.contains(a.first() + " == " + a.second())) - // format as "var == value" - .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) - // join with "&&" - .collect(Collectors.joining(" && ")); + List binderNames = getFound().getBinders(); + var assignments = counterexample.assignments().stream().filter(a -> binderNames.contains(a.first())) + .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first()))) + .toList(); - if (counterexampleString.isEmpty()) + if (assignments.isEmpty()) return null; - return counterexampleString; + return new Counterexample(assignments); } public Counterexample getCounterexample() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java index d70b2a77..e545b997 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java @@ -1,5 +1,8 @@ package liquidjava.rj_language.opt; +import java.util.ArrayList; +import java.util.List; + import liquidjava.processor.VCImplication; /** @@ -44,6 +47,17 @@ public String getSimplification() { return simplification; } + /** + * Returns the list of binder names in the simplified VC chain in order of appearance + */ + public List getBinders() { + ArrayList binderNames = new ArrayList<>(); + for (VCImplication current = getImplication(); current != null; current = current.getNext()) + if (current.hasBinder()) + binderNames.add(current.getName()); + return binderNames; + } + @Override public String toString() { if (origin == null) From 5811f3413e753fb000a72c61875f9f5660059505 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 14 Jul 2026 21:01:36 +0100 Subject: [PATCH 2/6] Filter Known Assignments --- .../java/liquidjava/diagnostics/errors/RefinementError.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index a3a6c940..75b4aea2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,11 +1,12 @@ package liquidjava.diagnostics.errors; -import java.util.ArrayList; import java.util.List; +import java.util.Set; import java.util.stream.Collectors; import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; @@ -60,7 +61,10 @@ public Counterexample getCounterExamples() { return null; List binderNames = getFound().getBinders(); + Set knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream() + .map(Expression::toString).collect(Collectors.toSet()); var assignments = counterexample.assignments().stream().filter(a -> binderNames.contains(a.first())) + .filter(a -> !knownAssignments.contains(a.first() + " == " + a.second())) .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first()))) .toList(); From 83d1f25922a9f725165713da3603035ab1b9e599 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Jul 2026 15:48:52 +0100 Subject: [PATCH 3/6] Refactor Counterexamples --- .../diagnostics/errors/RefinementError.java | 37 ++++++++++--------- 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 75b4aea2..b8583587 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -10,6 +10,7 @@ import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; +import liquidjava.utils.Pair; import spoon.reflect.cu.SourcePosition; /** @@ -34,7 +35,7 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi position, translationTable, customMessage); this.expected = expected; this.found = found; - this.counterexample = counterexample; + this.counterexample = filterCounterexample(counterexample); this.declarationPosition = declarationPosition; } @@ -45,25 +46,37 @@ public SourcePosition getDeclarationPosition() { @Override public String getDetails() { - Counterexample counterexamples = getCounterExamples(); - if (counterexamples == null) + if (counterexample == null) return ""; - String counterexampleString = counterexamples.assignments().stream() + String counterexampleString = counterexample.assignments().stream() .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) .collect(Collectors.joining(" && ")); return "Counterexample: " + counterexampleString; } + public Counterexample getCounterexample() { + return counterexample; + } + + public Predicate getExpected() { + return expected; + } + + public VCSimplificationResult getFound() { + return found; + } + // Filters counterexample assignments only in found VC and sorts them in the order of its binders - public Counterexample getCounterExamples() { + private Counterexample filterCounterexample(Counterexample counterexample) { if (counterexample == null || counterexample.assignments().isEmpty()) return null; List binderNames = getFound().getBinders(); Set knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream() .map(Expression::toString).collect(Collectors.toSet()); - var assignments = counterexample.assignments().stream().filter(a -> binderNames.contains(a.first())) + List> assignments = counterexample.assignments().stream() + .filter(a -> binderNames.contains(a.first())) .filter(a -> !knownAssignments.contains(a.first() + " == " + a.second())) .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first()))) .toList(); @@ -73,16 +86,4 @@ public Counterexample getCounterExamples() { return new Counterexample(assignments); } - - public Counterexample getCounterexample() { - return counterexample; - } - - public Predicate getExpected() { - return expected; - } - - public VCSimplificationResult getFound() { - return found; - } } From d5a0d84969e98ab6120bb816861c3b431e6cf61b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Jul 2026 17:48:59 +0100 Subject: [PATCH 4/6] Minor Improvements --- .../liquidjava/diagnostics/errors/RefinementError.java | 8 +------- .../src/main/java/liquidjava/smt/Counterexample.java | 3 +++ 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index b8583587..dc812c2d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -46,7 +46,7 @@ public SourcePosition getDeclarationPosition() { @Override public String getDetails() { - if (counterexample == null) + if (counterexample.isEmpty()) return ""; String counterexampleString = counterexample.assignments().stream() @@ -69,9 +69,6 @@ public VCSimplificationResult getFound() { // Filters counterexample assignments only in found VC and sorts them in the order of its binders private Counterexample filterCounterexample(Counterexample counterexample) { - if (counterexample == null || counterexample.assignments().isEmpty()) - return null; - List binderNames = getFound().getBinders(); Set knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream() .map(Expression::toString).collect(Collectors.toSet()); @@ -81,9 +78,6 @@ private Counterexample filterCounterexample(Counterexample counterexample) { .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first()))) .toList(); - if (assignments.isEmpty()) - return null; - return new Counterexample(assignments); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java b/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java index 3d72973e..93820e05 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java @@ -5,4 +5,7 @@ import liquidjava.utils.Pair; public record Counterexample(List> assignments) { + public boolean isEmpty() { + return assignments.isEmpty(); + } } From abdf80aded04778d637b7d1263669e56be3e1a43 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Jul 2026 18:14:48 +0100 Subject: [PATCH 5/6] Add Counterexample Tests --- .../src/main/java/testSuite/ErrorBoolean.java | 11 ++ .../testSuite/ErrorDependentRefinement.java | 2 +- .../testSuite/ErrorDependentUpperBound.java | 13 +++ .../main/java/testSuite/ErrorIdentity.java | 11 ++ .../java/testSuite/ErrorIntegerDivision.java | 11 ++ .../main/java/testSuite/ErrorLiteralZero.java | 11 ++ .../testSuite/ErrorRecursiveDecrement.java | 10 ++ .../api/tests/TestCounterexamples.java | 104 ++++++++++++++++++ 8 files changed, 172 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoolean.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorIdentity.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java new file mode 100644 index 00000000..486ab222 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java @@ -0,0 +1,11 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorBoolean { + + @Refinement("_ == true") + boolean mustBeTrue(boolean value) { + return value; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java index 42f18673..d593bc62 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java @@ -9,7 +9,7 @@ public static void main(String[] args) { int smaller = 5; @Refinement("bigger > 20") int bigger = 50; - @Refinement("_ > smaller && _ < bigger") + @Refinement("_ > smaller && _ < bigger") int middle = 21; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java new file mode 100644 index 00000000..0310089a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java @@ -0,0 +1,13 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorDependentUpperBound { + + @Refinement("0 <= _ && _ < len") + int nextIndex( + @Refinement("_ > 0") int len, + @Refinement("0 <= _ && _ < len") int i) { + return i + 1; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java b/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java new file mode 100644 index 00000000..a88c8091 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java @@ -0,0 +1,11 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorIdentity { + + @Refinement("_ > 0") + int positiveIdentity(int x) { + return x; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java b/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java new file mode 100644 index 00000000..6f6e616c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java @@ -0,0 +1,11 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorIntegerDivision { + + @Refinement("_ > 0") + int half(@Refinement("_ > 0") int x) { + return x / 2; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java b/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java new file mode 100644 index 00000000..8490425a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java @@ -0,0 +1,11 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorLiteralZero { + + @Refinement("_ != 0") + int zero() { + return 0; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java new file mode 100644 index 00000000..a9477c97 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java @@ -0,0 +1,10 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorRecursiveDecrement { + + public int f(@Refinement("_ > 0") int x) { + return f(x - 1); // Refinement Error + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java new file mode 100644 index 00000000..77fb3692 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -0,0 +1,104 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.RefinementError; +import liquidjava.utils.Pair; + +class TestCounterexamples { + + private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; + + @Test + void recursiveDecrementIncludesInputAndGeneratedArgument() { + RefinementError error = verify("ErrorRecursiveDecrement.java"); + assertAssignments(error, assignment("x", "1"), assignment("#x", "0")); + } + + @Test + void integerDivisionIncludesInputAndGeneratedReturn() { + RefinementError error = verify("ErrorIntegerDivision.java"); + assertAssignments(error, assignment("x", "1"), assignment("#ret", "0")); + } + + @Test + void dependentUpperBoundIncludesBoundaryValuesInBinderOrder() { + RefinementError error = verify("ErrorDependentUpperBound.java"); + assertAssignments(error, assignment("len", "1"), assignment("i", "0"), assignment("#ret", "1")); + } + + @Test + void literalZeroHasNoCounterexampleBecauseValueIsAlreadyKnown() { + RefinementError error = verify("ErrorLiteralZero.java"); + assertTrue(error.getCounterexample().isEmpty()); + } + + @Test + void identityRetainsInputAndReturnSelectedByTheModel() { + RefinementError error = verify("ErrorIdentity.java"); + assertAssignments(error, assignment("x", "0"), assignment("#ret", "0")); + } + + @Test + void staticFinalConstantHasNoCounterexampleBecauseValueIsAlreadyKnown() { + RefinementError error = verify("ErrorStaticFinalConstant.java"); + assertTrue(error.getCounterexample().isEmpty()); + } + + @Test + void knownReturnAssignmentIsRemovedWhileDependentAssignmentsRemain() { + RefinementError error = verify("ErrorDependentRefinement.java"); + assertAssignments(error, assignment("smaller", "0"), assignment("bigger", "21")); + } + + @Test + void multipleParametersAndGeneratedReturnFollowBinderOrder() { + RefinementError error = verify("ErrorFunctionDeclarations.java"); + assertAssignments(error, assignment("d", "0"), assignment("i", "1"), assignment("#ret", "2")); + } + + @Test + void variableUpdateIncludesNegativeInputAndGeneratedReturn() { + RefinementError error = verify("ErrorAssignmentBeforeReturn.java"); + assertAssignments(error, assignment("x", "-1"), assignment("#ret", "0")); + } + + @Test + void pathConditionIsOmittedWhileRecursiveArgumentRemains() { + RefinementError error = verify("ErrorRecursion.java"); + assertAssignments(error, assignment("k", "0"), assignment("#k", "-1")); + } + + @Test + void booleanCounterexampleIncludesInputAndGeneratedReturn() { + RefinementError error = verify("ErrorBoolean.java"); + assertAssignments(error, assignment("value", "false"), assignment("#ret", "false")); + } + + private static RefinementError verify(String test) { + CommandLineLauncher.launch(TEST_SUITE + test); + List errors = Diagnostics.getInstance().getErrors().stream().toList(); + assertEquals(1, errors.size(), "Expected exactly one error from " + test); + return assertInstanceOf(RefinementError.class, errors.getFirst()); + } + + @SafeVarargs + private static void assertAssignments(RefinementError error, Pair... expectedAssignments) { + // get counterexample assignments without instance numbers in variable names + List> actualAssignments = error.getCounterexample().assignments().stream() + .map(assignment -> assignment(assignment.first().replaceAll("_[0-9]+$", ""), assignment.second())) + .toList(); + assertEquals(List.of(expectedAssignments), actualAssignments); + } + + private static Pair assignment(String name, String value) { + return new Pair<>(name, value); + } +} From c703abae478a4937f4c8b9c3b5cf0db315381286 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Jul 2026 18:19:19 +0100 Subject: [PATCH 6/6] Remove Unused Imports --- .../java/liquidjava/processor/refinement_checker/VCChecker.java | 1 - .../src/test/java/liquidjava/api/tests/TestCounterexamples.java | 2 +- .../src/test/java/liquidjava/api/tests/TestExamples.java | 2 -- 3 files changed, 1 insertion(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 81c2b61f..b51d1c3e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -23,7 +23,6 @@ import liquidjava.smt.SMTResult; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; -import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java index 77fb3692..9d45cde0 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -86,7 +86,7 @@ private static RefinementError verify(String test) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList(); assertEquals(1, errors.size(), "Expected exactly one error from " + test); - return assertInstanceOf(RefinementError.class, errors.getFirst()); + return assertInstanceOf(RefinementError.class, errors.get(0)); } @SafeVarargs diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index c2464d70..e739915f 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -13,8 +13,6 @@ import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; -import liquidjava.diagnostics.errors.*; - import liquidjava.diagnostics.errors.LJError; import liquidjava.utils.Pair;