From 9869ee3c34fec3d973c6948f1bfd836c5c5e7df2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 22:50:34 +0000 Subject: [PATCH 1/7] Check Expected Errors in Tests --- .../liquidjava/api/tests/TestExamples.java | 72 +++++++++++-------- .../test/java/liquidjava/utils/TestUtils.java | 57 +++++++++++++++ 2 files changed, 100 insertions(+), 29 deletions(-) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java 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 f0822bef..50c25c0a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -1,15 +1,18 @@ package liquidjava.api.tests; +import static liquidjava.utils.TestUtils.*; import static org.junit.Assert.fail; import java.io.IOException; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; +import java.util.Optional; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; @@ -22,29 +25,48 @@ public class TestExamples { * Test the file at the given path by launching the verifier and checking for errors. The file/directory is expected * to be either correct or contain an error based on its name. * - * @param filePath + * @param path * path to the file to test */ @ParameterizedTest - @MethodSource("fileNameSource") - public void testFile(final Path filePath) { - String fileName = filePath.getFileName().toString(); + @MethodSource("sourcePaths") + public void testPath(final Path path) { + String pathName = path.getFileName().toString(); + boolean isDirectory = Files.isDirectory(path); - // 1. Run the verifier on the file or package - CommandLineLauncher.launch(filePath.toAbsolutePath().toString()); + // run verification + CommandLineLauncher.launch(path.toAbsolutePath().toString()); - // 2. Check if the file is correct or contains an error - if (isCorrect(fileName) && diagnostics.foundError()) { - if (fileName.toLowerCase().startsWith("warning")) { - System.out.println("Warning in directory: " + fileName + " --- should be correct with warnings"); - } - System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found"); + // verification should pass, check if any errors were found + if (shouldPass(pathName) && diagnostics.foundError()) { + System.out.println("Error in: " + pathName + " --- should be correct but an error was found"); fail(); } - // 3. Check if the file has an error but passed verification - if (isError(fileName) && !diagnostics.foundError()) { - System.out.println("Error in directory: " + fileName + " --- should be an error but passed verification"); - fail(); + // verification should fail, check if it failed as expected (we assume each error test has exactly one error) + else if (shouldFail(pathName)) { + if (!diagnostics.foundError()) { + System.out.println("Error in: " + pathName + " --- should be an error but passed verification"); + fail(); + } else { + // check if expected error was found + Optional expected = isDirectory ? getExpectedErrorFromDirectory(path) + : getExpectedErrorFromFile(path); + if (diagnostics.getErrors().size() > 1) { + System.out.println("Multiple errors found in: " + pathName + " --- expected exactly one error"); + fail(); + } + LJError error = diagnostics.getErrors().iterator().next(); + if (expected.isPresent()) { + String expectedMsg = expected.get(); + if (!error.getTitle().equals(expectedMsg)) { + System.out.println("Error in: " + pathName + " --- expected error: " + expectedMsg + + ", but found: " + error.getTitle()); + fail(); + } + } else { + System.out.println("No expected error message found for: " + pathName); + } + } } } @@ -57,17 +79,17 @@ public void testFile(final Path filePath) { * @throws IOException * if an I/O error occurs or the path does not exist */ - private static Stream fileNameSource() throws IOException { + private static Stream sourcePaths() throws IOException { return Files.find(Paths.get("../liquidjava-example/src/main/java/testSuite/"), Integer.MAX_VALUE, (filePath, fileAttr) -> { String name = filePath.getFileName().toString(); - // 1. Files that start with "Correct" or "Error" + // Files that start with "Correct" or "Error" boolean isFileStartingWithCorrectOrError = fileAttr.isRegularFile() - && (isCorrect(name) || isError(name)); + && (shouldPass(name) || shouldFail(name)); - // 2. Folders (directories) that contain "correct" or "error" + // Directories that contain "correct" or "error" boolean isDirectoryWithCorrectOrError = fileAttr.isDirectory() - && (isCorrect(name) || isError(name)); + && (shouldPass(name) || shouldFail(name)); // Return true if either condition matches return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError; @@ -89,12 +111,4 @@ public void testMultiplePaths() { fail(); } } - - private static boolean isCorrect(String path) { - return path.toLowerCase().contains("correct") || path.toLowerCase().contains("warning"); - } - - private static boolean isError(String path) { - return path.toLowerCase().contains("error"); - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java new file mode 100644 index 00000000..74d1caec --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -0,0 +1,57 @@ +package liquidjava.utils; + +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.Optional; +import java.util.stream.Stream; + +public class TestUtils { + + public static boolean shouldPass(String path) { + return path.toLowerCase().contains("correct") || path.toLowerCase().contains("warning"); + } + + public static boolean shouldFail(String path) { + return path.toLowerCase().contains("error"); + } + + /** + * Reads the expected error message from the first line of the given test file + * + * @param filePath + * + * @return optional containing the expected error message if present, otherwise empty + */ + public static Optional getExpectedErrorFromFile(Path filePath) { + try (Stream lines = Files.lines(filePath)) { + Optional first = lines.findFirst(); + if (first.isPresent() && first.get().startsWith("//")) { + return Optional.of(first.get().substring(2).trim()); + } else { + return Optional.empty(); + } + } catch (Exception e) { + return Optional.empty(); + } + } + + /** + * Reads the expected error message from a .expected file in the given directory + * + * @param dirPath + * + * @return optional containing the expected error message if present, otherwise empty + */ + public static Optional getExpectedErrorFromDirectory(Path dirPath) { + Path expectedFilePath = dirPath.resolve(".expected"); + if (Files.exists(expectedFilePath)) { + try (Stream lines = Files.lines(expectedFilePath)) { + return lines.findFirst().map(String::trim); + } catch (IOException e) { + return Optional.empty(); + } + } + return Optional.empty(); + } +} From 333c6e07e927a7ceec87461d812248a68a3dce5e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 23:10:30 +0000 Subject: [PATCH 2/7] Add Expected Errors --- .../src/main/java/testSuite/ErrorAfterIf.java | 1 + .../src/main/java/testSuite/ErrorAfterIf2.java | 1 + .../src/main/java/testSuite/ErrorAlias.java | 1 + .../src/main/java/testSuite/ErrorAliasArgumentSize.java | 3 ++- .../src/main/java/testSuite/ErrorAliasSimple.java | 1 + .../src/main/java/testSuite/ErrorAliasTypeMismatch.java | 1 + .../java/testSuite/ErrorArithmeticBinaryOperations.java | 1 + .../src/main/java/testSuite/ErrorArithmeticFP1.java | 1 + .../src/main/java/testSuite/ErrorArithmeticFP2.java | 1 + .../src/main/java/testSuite/ErrorArithmeticFP3.java | 1 + .../src/main/java/testSuite/ErrorArithmeticFP4.java | 1 + .../java/testSuite/ErrorAssignementAfterDeclaration.java | 1 + .../main/java/testSuite/ErrorBooleanFunInvocation.java | 1 + .../src/main/java/testSuite/ErrorBooleanLiteral.java | 1 + .../src/main/java/testSuite/ErrorDependentRefinement.java | 1 + .../main/java/testSuite/ErrorFunctionDeclarations.java | 1 + .../src/main/java/testSuite/ErrorFunctionInvocation.java | 1 + .../src/main/java/testSuite/ErrorFunctionInvocation1.java | 1 + .../java/testSuite/ErrorFunctionInvocationParams.java | 1 + .../src/main/java/testSuite/ErrorGhostArgsTypes.java | 1 + .../src/main/java/testSuite/ErrorGhostNumberArgs.java | 1 + .../src/main/java/testSuite/ErrorIfAssignment.java | 1 + .../src/main/java/testSuite/ErrorIfAssignment2.java | 1 + .../testSuite/ErrorImplementationSearchValueIntArray.java | 1 + .../src/main/java/testSuite/ErrorLenZeroIntArray.java | 1 + .../src/main/java/testSuite/ErrorLongUsage1.java | 1 + .../src/main/java/testSuite/ErrorLongUsage2.java | 1 + .../java/testSuite/ErrorMissingAliasTypeParameter.java | 1 + .../src/main/java/testSuite/ErrorNoRefinementsInVar.java | 1 + .../src/main/java/testSuite/ErrorRecursion1.java | 1 + .../src/main/java/testSuite/ErrorSearchIntArray.java | 1 + .../main/java/testSuite/ErrorSearchValueIntArray1.java | 1 + .../main/java/testSuite/ErrorSearchValueIntArray2.java | 1 + .../src/main/java/testSuite/ErrorSimpleAssignment.java | 1 + .../src/main/java/testSuite/ErrorSpecificArithmetic.java | 1 + .../src/main/java/testSuite/ErrorSpecificValuesIf.java | 1 + .../src/main/java/testSuite/ErrorSpecificValuesIf2.java | 1 + .../main/java/testSuite/ErrorSpecificVarInRefinement.java | 1 + .../java/testSuite/ErrorSpecificVarInRefinementIf.java | 1 + .../src/main/java/testSuite/ErrorSyntax1.java | 1 + .../src/main/java/testSuite/ErrorTernaryExpression.java | 1 + .../src/main/java/testSuite/ErrorTrafficLightRGB.java | 1 + .../src/main/java/testSuite/ErrorTypeInRefinements.java | 1 + .../src/main/java/testSuite/ErrorUnaryOpMinus.java | 1 + .../src/main/java/testSuite/ErrorUnaryOperators.java | 1 + .../src/main/java/testSuite/classes/ErrorGhostState.java | 1 + .../java/testSuite/classes/boolean_ghost_error/.expected | 1 + .../src/main/java/testSuite/classes/email_error/.expected | 1 + .../testSuite/classes/index_out_of_bounds_error/.expected | 1 + .../java/testSuite/classes/input_reader_error/.expected | 1 + .../java/testSuite/classes/input_reader_error2/.expected | 1 + .../main/java/testSuite/classes/iterator_error/.expected | 1 + .../testSuite/classes/method_overload_error/.expected | 1 + .../java/testSuite/classes/order_gift_error/.expected | 1 + .../testSuite/classes/refs_from_interface_error/.expected | 1 + .../classes/refs_from_superclass_error/.expected | 1 + .../java/testSuite/classes/scoreboard_error/.expected | 1 + .../main/java/testSuite/classes/socket_error/.expected | 1 + .../java/testSuite/classes/state_multiple_error/.expected | 1 + .../java/testSuite/field_updates/ErrorFieldUpdate.java | 1 + .../src/main/java/testSuite/math/errorAbs/.expected | 1 + .../src/main/java/testSuite/math/errorMax/.expected | 1 + .../main/java/testSuite/math/errorMultiplyExact/.expected | 1 + .../refinement_checker/ExternalRefinementTypeChecker.java | 8 ++++---- .../src/test/java/liquidjava/api/tests/TestExamples.java | 3 +++ 65 files changed, 71 insertions(+), 5 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/email_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/math/errorMax/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java index 130434f9..fd375b09 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java index b6a0816f..3ae6ed8e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java index 4cc2b496..7ed25815 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java index 6e3682cd..4e68cd6b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -8,7 +9,7 @@ public class ErrorAliasArgumentSize { public static void main(String[] args) { - @Refinement("InRange( _, 10)") + @Refinement("InRange(_, 0, 10)") int j = 15; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java index ce751d5c..1e2f1787 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java index 074765a0..1131b73f 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java index 9556fea0..b2add7fa 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java index b5798484..45239bc6 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java index ab60cb9b..16e58df7 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java index 0e96412d..ae85bc50 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java index 51706603..88eed94c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java index 83b31147..60acfbd7 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java index 029fd4dc..99cc67d6 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java index 0ad3ded1..09b97f7e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java index d8d5715d..9c83af5e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java index 99f6f435..e2184b67 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java index a8439044..f1ca6bf7 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java index 26119616..e4309a4c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java index ba398c67..6d1fa473 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java index 5fce2f7d..207e3edd 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java @@ -1,3 +1,4 @@ +// Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java index f080428c..b46a1a70 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java @@ -1,3 +1,4 @@ +// Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java index 90c225c5..06c61126 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java index c66c4b71..19692a5a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java index e34f2c4d..41061023 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java index 04e2f523..2aadc688 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java index aef298bb..2bc1d1f6 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java index 61a482d3..fe5a231a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java index 52c2c758..f53bf558 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java @@ -1,3 +1,4 @@ +// Syntax Error package testSuite; import liquidjava.specification.RefinementAlias; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java b/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java index 2db74f88..c2133b27 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java index 7b5b9fe6..518d351e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java index e25c2c13..54ac3507 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java index ad63b279..f7a96890 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java index d9f482ea..944b7e6f 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java index a00d4069..d07f1259 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java index 1a63afc4..65bdde9b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java index b15b633e..04704a8e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java index c1e373c3..2cae544c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java index 6ec09838..ccb34136 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java index 7e1d1c22..c00f5b90 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java index bdf498ae..6d28e95c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java @@ -1,3 +1,4 @@ +// Syntax Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java b/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java index 4543463b..2c89393a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java index 018db95a..3b50f615 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java @@ -1,3 +1,4 @@ +// State Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java index 6583832f..2981a217 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java @@ -1,3 +1,4 @@ +// Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java index 85149333..73eb1529 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java index dbc59590..b8660ea8 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java @@ -1,3 +1,4 @@ +// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java index 6580fab7..80e2741c 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java +++ b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java @@ -1,3 +1,4 @@ +// Error package testSuite.classes; import liquidjava.specification.Ghost; diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected new file mode 100644 index 00000000..6f476981 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected @@ -0,0 +1 @@ +Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected new file mode 100644 index 00000000..6f476981 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected @@ -0,0 +1 @@ +Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected new file mode 100644 index 00000000..6f476981 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected @@ -0,0 +1 @@ +Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected new file mode 100644 index 00000000..6f476981 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected @@ -0,0 +1 @@ +Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected new file mode 100644 index 00000000..258d98bb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected @@ -0,0 +1 @@ +State Conflict Error diff --git a/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java b/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java index 4aeaf01e..55a10184 100644 --- a/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java +++ b/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java @@ -1,3 +1,4 @@ +// State Refinement Error package testSuite.field_updates; import liquidjava.specification.StateRefinement; diff --git a/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected b/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected new file mode 100644 index 00000000..6f476981 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected @@ -0,0 +1 @@ +Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected b/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected new file mode 100644 index 00000000..6f476981 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected @@ -0,0 +1 @@ +Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected new file mode 100644 index 00000000..6f476981 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected @@ -0,0 +1 @@ +Refinement Error diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 7bd910b6..5773a548 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -71,16 +71,16 @@ public void visitCtMethod(CtMethod method) { String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); - diagnostics.add( - new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), prefix, overloads)); + diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), + prefix, overloads)); } } else { if (!methodExists(targetType, method)) { String message = String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); - diagnostics.add( - new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), prefix, overloads)); + diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), + prefix, overloads)); return; } } 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 50c25c0a..26c8bbf5 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -65,6 +65,9 @@ else if (shouldFail(pathName)) { } } else { System.out.println("No expected error message found for: " + pathName); + System.out.println("Please provide an expected error in " + (isDirectory + ? "a .expected file in the directory" : "the first line of the test file as a comment")); + fail(); } } } From 6df142a4e76cae2d8d6453944127e98f5f6ab33e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 23:17:26 +0000 Subject: [PATCH 3/7] Case Insensitive Comparison of Expected Error --- .../src/test/java/liquidjava/api/tests/TestExamples.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 26c8bbf5..3242f559 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -57,8 +57,8 @@ else if (shouldFail(pathName)) { } LJError error = diagnostics.getErrors().iterator().next(); if (expected.isPresent()) { - String expectedMsg = expected.get(); - if (!error.getTitle().equals(expectedMsg)) { + String expectedMsg = expected.get().toLowerCase(); + if (!error.getTitle().toLowerCase().equals(expectedMsg)) { System.out.println("Error in: " + pathName + " --- expected error: " + expectedMsg + ", but found: " + error.getTitle()); fail(); From a8703066b7590b319a76e16b4224384793844f86 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 23:26:42 +0000 Subject: [PATCH 4/7] Minor Changes --- .../src/test/java/liquidjava/api/tests/TestExamples.java | 4 ++-- .../src/test/java/liquidjava/utils/TestUtils.java | 8 ++++++++ 2 files changed, 10 insertions(+), 2 deletions(-) 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 3242f559..9b2925c4 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -39,13 +39,13 @@ public void testPath(final Path path) { // verification should pass, check if any errors were found if (shouldPass(pathName) && diagnostics.foundError()) { - System.out.println("Error in: " + pathName + " --- should be correct but an error was found"); + System.out.println("Error in: " + pathName + " --- should pass but an error was found"); fail(); } // verification should fail, check if it failed as expected (we assume each error test has exactly one error) else if (shouldFail(pathName)) { if (!diagnostics.foundError()) { - System.out.println("Error in: " + pathName + " --- should be an error but passed verification"); + System.out.println("Error in: " + pathName + " --- should fail but no errors were found"); fail(); } else { // check if expected error was found diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 74d1caec..9b05725e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -8,10 +8,18 @@ public class TestUtils { + /** + * Determines if the given path indicates that the test should pass + * @param path + */ public static boolean shouldPass(String path) { return path.toLowerCase().contains("correct") || path.toLowerCase().contains("warning"); } + /** + * Determines if the given path indicates that the test should fail + * @param path + */ public static boolean shouldFail(String path) { return path.toLowerCase().contains("error"); } From e1eecc6026c58c6c19871f9848eb3f5713eb8ed0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 22 Nov 2025 12:02:56 +0000 Subject: [PATCH 5/7] Update Test --- .../src/main/java/testSuite/ErrorAliasArgumentSize.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java index 4e68cd6b..bdf527c5 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java @@ -1,4 +1,4 @@ -// Refinement Error +// Not Found Error package testSuite; import liquidjava.specification.Refinement; @@ -9,7 +9,7 @@ public class ErrorAliasArgumentSize { public static void main(String[] args) { - @Refinement("InRange(_, 0, 10)") + @Refinement("InRange(j, 10)") int j = 15; } } From cc9bade951206f59439b9f68c4d774d706bd8e5e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 22 Nov 2025 19:47:07 +0000 Subject: [PATCH 6/7] Minor Change --- .../src/test/java/liquidjava/api/tests/TestExamples.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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 9b2925c4..be0f1ca0 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -57,10 +57,11 @@ else if (shouldFail(pathName)) { } LJError error = diagnostics.getErrors().iterator().next(); if (expected.isPresent()) { - String expectedMsg = expected.get().toLowerCase(); - if (!error.getTitle().toLowerCase().equals(expectedMsg)) { - System.out.println("Error in: " + pathName + " --- expected error: " + expectedMsg - + ", but found: " + error.getTitle()); + String expectedError = expected.get(); + String foundError = error.getTitle(); + if (!foundError.equalsIgnoreCase(expectedError)) { + System.out.println("Error in: " + pathName + " --- expected error: " + expectedError + + ", but found: " + foundError); fail(); } } else { From d6672a7e45dc1b1f65636a03a40a3af7c3a02898 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 4 Dec 2025 11:21:37 +0000 Subject: [PATCH 7/7] Update README --- README.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 1e20ac80..1c51a532 100644 --- a/README.md +++ b/README.md @@ -78,8 +78,6 @@ To run LiquidJava, use the Maven command below, replacing `/path/to/your/project ```bash mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project" ``` -*Warning: Any change to LiquidJava requires rebuilding the jar.* - If you're on Linux/macOS, you can use the `liquidjava` script (from the repository root) to simplify the process. @@ -105,10 +103,14 @@ The starter test file is `TestExamples.java`, which runs the test suite under th The test suite considers test cases: 1. Files that start with `Correct` or `Error` (e.g., `CorrectRecursion.java`) -2. Packages or folders that contain the word `correct` or `error` (e.g., `arraylist_correct`) +2. Directories that contain the word `correct` or `error` (e.g., `arraylist_correct`) Therefore, the files and folders that do not follow this pattern are ignored. +For failing test cases, the expected error must be specified as follows: +1. In singular test files, the expected error (title) should be written in the first line of the file as a comment +2. In test directories, a `.expected` file should be included in that directory with the expected error (title) + ## Project Structure * **docs**: Contains documents used for the design of the language. This folder includes a [README](./docs/design/README.md) with the link to the full artifact used in the design process. It also contains initial documents used to prepare the design of the refinements language during its evaluation