From 66952cca0e21481cbf0fbb8ba680fa5620c6ce57 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 12 Sep 2026 22:46:22 +0100 Subject: [PATCH 1/8] Inline Expected Warnings in Tests --- .../WarningExtRefNonExistentClass.java | 2 +- .../WarningExtRefNonExistentMethod.java | 2 +- .../WarningExtRefWrongConstructor.java | 2 +- .../WarningExtRefWrongParameterType.java | 2 +- .../testSuite/WarningExtRefWrongRetType.java | 2 +- .../liquidjava/api/tests/TestExamples.java | 33 +++++++++-- .../test/java/liquidjava/utils/TestUtils.java | 58 +++++++++++++++++++ 7 files changed, 90 insertions(+), 11 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java index b79eaa870..6d0fd1fd1 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java @@ -2,7 +2,7 @@ import liquidjava.specification.ExternalRefinementsFor; -@ExternalRefinementsFor("non.existent.Class") +@ExternalRefinementsFor("non.existent.Class") // Warning public interface WarningExtRefNonExistentClass { public void NonExistentClass(); } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java index 08d81de91..e1794c589 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java @@ -12,5 +12,5 @@ public interface WarningExtRefNonExistentMethod { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public boolean adddd(E e); + public boolean adddd(E e); // Warning } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java index 576a70e9e..76b0a4c4b 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java @@ -9,7 +9,7 @@ public interface WarningExtRefWrongConstructor { @StateRefinement(to = "size(this) == 0") - public void ArrayList(String wrongParameter); + public void ArrayList(String wrongParameter); // Warning @StateRefinement(to = "size(this) == (size(old(this)) + 1)") public boolean add(E e); diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java index 988c465f4..5b31471b7 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java @@ -12,5 +12,5 @@ public interface WarningExtRefWrongParameterType { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public boolean add(int wrongParameter); + public boolean add(int wrongParameter); // Warning } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java index 97477b2ae..61994d53a 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java @@ -12,5 +12,5 @@ public interface WarningExtRefWrongRetType { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public int add(E e); // wrong return type + public int add(E e); // Warning } 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 e739915fb..810b32955 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -14,6 +14,7 @@ import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.warnings.LJWarning; import liquidjava.utils.Pair; import org.junit.Test; @@ -25,8 +26,8 @@ public class TestExamples { Diagnostics diagnostics = Diagnostics.getInstance(); /** - * 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. + * Test the file at the given path by launching the verifier and checking for errors and warnings. The + * file/directory is expected to be either correct, contain an error, or report warnings based on its name. * * @param path * path to the file to test @@ -40,6 +41,26 @@ public void testPath(final Path path) { // run verification CommandLineLauncher.launch(path.toFile().toString()); + List> expectedWarnings = isDirectory ? getExpectedWarningsFromDirectory(path) + : getExpectedWarningsFromFile(path); + + if (shouldWarn(pathName)) { + if (diagnostics.getWarnings().size() != expectedWarnings.size()) { + System.out.println("Warnings found in: " + pathName + " --- expected exactly " + expectedWarnings.size() + + " warnings. \n" + diagnostics.getWarningOutput()); + fail(); + } + for (LJWarning warning : diagnostics.getWarnings()) { + int warningPosition = warning.getPosition().getLine(); + boolean match = expectedWarnings.stream().anyMatch(expected -> expected.second() == warningPosition); + if (!match) { + System.out.println("Warning in: " + pathName + " --- expected warnings: " + expectedWarnings + + ", but found one at " + warningPosition + ". \n" + diagnostics.getWarningOutput()); + fail(); + } + } + } + // verification should pass, check if any errors were found if (shouldPass(pathName) && diagnostics.foundError()) { System.out.println("Error in: " + pathName + " --- should pass but an error was found. \n" @@ -98,13 +119,13 @@ 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(); - // Files that start with "Correct" or "Error" + // Files that start with "Correct", "Error" or "Warning" boolean isFileStartingWithCorrectOrError = fileAttr.isRegularFile() - && (shouldPass(name) || shouldFail(name)); + && (shouldPass(name) || shouldFail(name) || shouldWarn(name)); - // Directories that contain "correct" or "error" + // Directories that contain "correct", "error" or "warning" boolean isDirectoryWithCorrectOrError = fileAttr.isDirectory() - && (shouldPass(name) || shouldFail(name)); + && (shouldPass(name) || shouldFail(name) || shouldWarn(name)); // Return true if either condition matches return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError; diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index f81f013fc..aa2297112 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -37,6 +37,15 @@ public static boolean shouldFail(String path) { return path.toLowerCase().contains("error"); } + /** + * Determines if the given path indicates that the test should report warnings + * + * @param path + */ + public static boolean shouldWarn(String path) { + return path.toLowerCase().contains("warning"); + } + /** * Reads the expected error messages from the given file by looking for a comment containing the expected error * message. @@ -65,6 +74,34 @@ public static List> getExpectedErrorsFromFile(Path filePat return expectedErrors; } + /** + * Reads the expected warning messages from the given file by looking for a comment containing the expected warning + * message. + * + * @param filePath + * + * @return list of expected warning messages found in the file, or empty list if there was an error reading the file + * or if there are no expected warning messages in the file + */ + public static List> getExpectedWarningsFromFile(Path filePath) { + List> expectedWarnings = new ArrayList<>(); + try (BufferedReader reader = Files.newBufferedReader(filePath)) { + String line; + int lineNumber = 0; + while ((line = reader.readLine()) != null) { + lineNumber++; + Pattern p = Pattern.compile("//\\s*(.*?\\bWarning\\b)", Pattern.CASE_INSENSITIVE); + Matcher m = p.matcher(line); + if (m.find()) { + expectedWarnings.add(new Pair<>(m.group(1).trim(), lineNumber)); + } + } + } catch (IOException e) { + return List.of(); + } + return expectedWarnings; + } + /** * Reads the expected error messages from all files in the given directory and combines them into a single list * @@ -86,6 +123,27 @@ public static List> getExpectedErrorsFromDirectory(Path di return expectedErrors; } + /** + * Reads the expected warning messages from all files in the given directory and combines them into a single list. + * + * @param dirPath + * + * @return list of expected warning messages from all files in the directory, or empty list if there was an error + * reading the directory or if there are no files in the directory + */ + public static List> getExpectedWarningsFromDirectory(Path dirPath) { + List> expectedWarnings = new ArrayList<>(); + try { + List files = Files.list(dirPath).filter(Files::isRegularFile).toList(); + for (Path file : files) { + expectedWarnings.addAll(getExpectedWarningsFromFile(file)); + } + } catch (IOException e) { + return List.of(); + } + return expectedWarnings; + } + /** * Helper method to add an integer variable to the context */ From 798f6f921281435066b8148e4409a885c95c68e8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 12 Sep 2026 23:00:00 +0100 Subject: [PATCH 2/8] Code Refactoring --- .../liquidjava/api/tests/TestExamples.java | 75 +++++++++---------- .../test/java/liquidjava/utils/TestUtils.java | 55 +++++--------- 2 files changed, 55 insertions(+), 75 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 810b32955..2440b5905 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -8,13 +8,14 @@ import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; +import java.util.Collection; import java.util.List; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.LJDiagnostic; import liquidjava.diagnostics.errors.LJError; -import liquidjava.diagnostics.warnings.LJWarning; import liquidjava.utils.Pair; import org.junit.Test; @@ -45,20 +46,8 @@ public void testPath(final Path path) { : getExpectedWarningsFromFile(path); if (shouldWarn(pathName)) { - if (diagnostics.getWarnings().size() != expectedWarnings.size()) { - System.out.println("Warnings found in: " + pathName + " --- expected exactly " + expectedWarnings.size() - + " warnings. \n" + diagnostics.getWarningOutput()); - fail(); - } - for (LJWarning warning : diagnostics.getWarnings()) { - int warningPosition = warning.getPosition().getLine(); - boolean match = expectedWarnings.stream().anyMatch(expected -> expected.second() == warningPosition); - if (!match) { - System.out.println("Warning in: " + pathName + " --- expected warnings: " + expectedWarnings - + ", but found one at " + warningPosition + ". \n" + diagnostics.getWarningOutput()); - fail(); - } - } + checkExpectedDiagnostics(pathName, diagnostics.getWarnings(), expectedWarnings, + diagnostics.getWarningOutput()); } // verification should pass, check if any errors were found @@ -77,35 +66,41 @@ else if (shouldFail(pathName)) { // check if expected error was found List> expectedErrors = isDirectory ? getExpectedErrorsFromDirectory(path) : getExpectedErrorsFromFile(path); - if (diagnostics.getErrors().size() != expectedErrors.size()) { - System.out.println("Multiple errors found in: " + pathName + " --- expected exactly " - + expectedErrors.size() + " errors. \n" + diagnostics.getErrorOutput()); - fail(); - } - if (!expectedErrors.isEmpty()) { - for (LJError e : diagnostics.getErrors()) { - String foundError = e.getTitle(); - int errorPosition = e.getPosition().getLine(); - boolean match = expectedErrors.stream().anyMatch( - expected -> expected.first().equals(foundError) && expected.second() == errorPosition); - - if (!match) { - System.out.println("Error in: " + pathName + " --- expected errors: " + expectedErrors - + ", but found: " + foundError + " at " + errorPosition + ". \n" - + diagnostics.getErrorOutput()); - fail(); - } - } - } else { - System.out.println("No expected error messages found for: " + pathName); - System.out.println( - "Please specify each expected error in the test file as a comment on the line where the error should be reported."); - fail(); - } + checkExpectedDiagnostics(pathName, diagnostics.getErrors(), expectedErrors, + diagnostics.getErrorOutput()); + } + } + } + + private static void checkExpectedDiagnostics(String pathName, Collection found, + List> expected, String output) { + if (found.size() != expected.size()) { + System.out.println("Unexpected number of diagnostics found in: " + pathName + " --- expected exactly " + + expected.size() + ". \n" + output); + fail(); + } + if (expected.isEmpty()) { + System.out.println("No expected diagnostic messages found for: " + pathName); + System.out.println( + "Please specify each expected diagnostic in the test file as a comment on the line where it should be reported."); + fail(); + } + for (LJDiagnostic diagnostic : found) { + boolean match = expected.stream().anyMatch(expectedDiagnostic -> matches(diagnostic, expectedDiagnostic)); + if (!match) { + System.out.println( + "Unexpected diagnostic in: " + pathName + " --- expected: " + expected + ". \n" + output); + fail(); } } } + private static boolean matches(LJDiagnostic diagnostic, Pair expected) { + if (diagnostic.getPosition().getLine() != expected.second()) + return false; + return !(diagnostic instanceof LJError) || diagnostic.getTitle().equals(expected.first()); + } + /** * Returns a Stream of paths to test files in the testSuite directory. These include files with names starting with * "Correct" or "Error", and directories containing "correct" or "error". § diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index aa2297112..2b3b662bb 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -16,6 +16,8 @@ public class TestUtils { + private static final Pattern EXPECTED_DIAGNOSTIC = Pattern.compile("//\\s*(.*?\\b(Error|Warning)\\b)", + Pattern.CASE_INSENSITIVE); private final static Factory factory = new Launcher().getFactory(); private final static Context context = Context.getInstance(); @@ -56,22 +58,25 @@ public static boolean shouldWarn(String path) { * or if there are no expected error messages in the file */ public static List> getExpectedErrorsFromFile(Path filePath) { - List> expectedErrors = new ArrayList<>(); + return getExpectedDiagnosticsFromFile(filePath, "error"); + } + + private static List> getExpectedDiagnosticsFromFile(Path filePath, String type) { + List> expectedDiagnostics = new ArrayList<>(); try (BufferedReader reader = Files.newBufferedReader(filePath)) { String line; int lineNumber = 0; while ((line = reader.readLine()) != null) { lineNumber++; - Pattern p = Pattern.compile("//\\s*(.*?\\bError\\b)", Pattern.CASE_INSENSITIVE); - Matcher m = p.matcher(line); - if (m.find()) { - expectedErrors.add(new Pair<>(m.group(1).trim(), lineNumber)); + Matcher matcher = EXPECTED_DIAGNOSTIC.matcher(line); + if (matcher.find() && matcher.group(2).equalsIgnoreCase(type)) { + expectedDiagnostics.add(new Pair<>(matcher.group(1).trim(), lineNumber)); } } } catch (IOException e) { return List.of(); } - return expectedErrors; + return expectedDiagnostics; } /** @@ -84,22 +89,7 @@ public static List> getExpectedErrorsFromFile(Path filePat * or if there are no expected warning messages in the file */ public static List> getExpectedWarningsFromFile(Path filePath) { - List> expectedWarnings = new ArrayList<>(); - try (BufferedReader reader = Files.newBufferedReader(filePath)) { - String line; - int lineNumber = 0; - while ((line = reader.readLine()) != null) { - lineNumber++; - Pattern p = Pattern.compile("//\\s*(.*?\\bWarning\\b)", Pattern.CASE_INSENSITIVE); - Matcher m = p.matcher(line); - if (m.find()) { - expectedWarnings.add(new Pair<>(m.group(1).trim(), lineNumber)); - } - } - } catch (IOException e) { - return List.of(); - } - return expectedWarnings; + return getExpectedDiagnosticsFromFile(filePath, "warning"); } /** @@ -111,16 +101,7 @@ public static List> getExpectedWarningsFromFile(Path fileP * reading the directory or if there are no files in the directory */ public static List> getExpectedErrorsFromDirectory(Path dirPath) { - List> expectedErrors = new ArrayList<>(); - try { - List files = Files.list(dirPath).filter(Files::isRegularFile).toList(); - for (Path file : files) { - expectedErrors.addAll(getExpectedErrorsFromFile(file)); - } - } catch (IOException e) { - return List.of(); - } - return expectedErrors; + return getExpectedDiagnosticsFromDirectory(dirPath, "error"); } /** @@ -132,16 +113,20 @@ public static List> getExpectedErrorsFromDirectory(Path di * reading the directory or if there are no files in the directory */ public static List> getExpectedWarningsFromDirectory(Path dirPath) { - List> expectedWarnings = new ArrayList<>(); + return getExpectedDiagnosticsFromDirectory(dirPath, "warning"); + } + + private static List> getExpectedDiagnosticsFromDirectory(Path dirPath, String type) { + List> expectedDiagnostics = new ArrayList<>(); try { List files = Files.list(dirPath).filter(Files::isRegularFile).toList(); for (Path file : files) { - expectedWarnings.addAll(getExpectedWarningsFromFile(file)); + expectedDiagnostics.addAll(getExpectedDiagnosticsFromFile(file, type)); } } catch (IOException e) { return List.of(); } - return expectedWarnings; + return expectedDiagnostics; } /** From 097591f9764607d7090055adadf8dd4390cf1cfb Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 12 Sep 2026 23:07:29 +0100 Subject: [PATCH 3/8] Update Javadocs --- .../liquidjava/api/tests/TestExamples.java | 20 ++----- .../test/java/liquidjava/utils/TestUtils.java | 58 +------------------ 2 files changed, 8 insertions(+), 70 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 2440b5905..f088afbe6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -27,11 +27,7 @@ public class TestExamples { Diagnostics diagnostics = Diagnostics.getInstance(); /** - * Test the file at the given path by launching the verifier and checking for errors and warnings. The - * file/directory is expected to be either correct, contain an error, or report warnings based on its name. - * - * @param path - * path to the file to test + * Runs the verifier and checks the expected diagnostics */ @ParameterizedTest @MethodSource("sourcePaths") @@ -72,6 +68,9 @@ else if (shouldFail(pathName)) { } } + /** + * Checks that the found diagnostics match the expected diagnostics + */ private static void checkExpectedDiagnostics(String pathName, Collection found, List> expected, String output) { if (found.size() != expected.size()) { @@ -102,13 +101,7 @@ private static boolean matches(LJDiagnostic diagnostic, Pair ex } /** - * Returns a Stream of paths to test files in the testSuite directory. These include files with names starting with - * "Correct" or "Error", and directories containing "correct" or "error". § - * - * @return Stream of paths to test files - * - * @throws IOException - * if an I/O error occurs or the path does not exist + * Returns the test suite paths to verify */ private static Stream sourcePaths() throws IOException { return Files.find(Paths.get("../liquidjava-example/src/main/java/testSuite/"), Integer.MAX_VALUE, @@ -128,8 +121,7 @@ private static Stream sourcePaths() throws IOException { } /** - * Test multiple paths at once, including both files and directories. This test ensures that the verifier can handle - * multiple inputs correctly and that no errors are found in files/directories that are expected to be correct. + * Verifies that multiple correct inputs can be processed together */ @Test public void testMultiplePaths() { diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 2b3b662bb..33ee09b2f 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -16,47 +16,22 @@ public class TestUtils { - private static final Pattern EXPECTED_DIAGNOSTIC = Pattern.compile("//\\s*(.*?\\b(Error|Warning)\\b)", - Pattern.CASE_INSENSITIVE); + private static final Pattern EXPECTED_DIAGNOSTIC = Pattern.compile("//\\s*(.*?\\b(Error|Warning)\\b)", Pattern.CASE_INSENSITIVE); private final static Factory factory = new Launcher().getFactory(); private final static Context context = Context.getInstance(); - /** - * Determines if the given path indicates that the test should pass - * - * @param path - */ public static boolean shouldPass(String path) { return path.toLowerCase().contains("correct"); } - /** - * Determines if the given path indicates that the test should fail - * - * @param path - */ public static boolean shouldFail(String path) { return path.toLowerCase().contains("error"); } - /** - * Determines if the given path indicates that the test should report warnings - * - * @param path - */ public static boolean shouldWarn(String path) { return path.toLowerCase().contains("warning"); } - /** - * Reads the expected error messages from the given file by looking for a comment containing the expected error - * message. - * - * @param filePath - * - * @return list of expected error messages found in the file, or empty list if there was an error reading the file - * or if there are no expected error messages in the file - */ public static List> getExpectedErrorsFromFile(Path filePath) { return getExpectedDiagnosticsFromFile(filePath, "error"); } @@ -79,39 +54,14 @@ private static List> getExpectedDiagnosticsFromFile(Path f return expectedDiagnostics; } - /** - * Reads the expected warning messages from the given file by looking for a comment containing the expected warning - * message. - * - * @param filePath - * - * @return list of expected warning messages found in the file, or empty list if there was an error reading the file - * or if there are no expected warning messages in the file - */ public static List> getExpectedWarningsFromFile(Path filePath) { return getExpectedDiagnosticsFromFile(filePath, "warning"); } - /** - * Reads the expected error messages from all files in the given directory and combines them into a single list - * - * @param dirPath - * - * @return list of expected error messages from all files in the directory, or empty list if there was an error - * reading the directory or if there are no files in the directory - */ public static List> getExpectedErrorsFromDirectory(Path dirPath) { return getExpectedDiagnosticsFromDirectory(dirPath, "error"); } - /** - * Reads the expected warning messages from all files in the given directory and combines them into a single list. - * - * @param dirPath - * - * @return list of expected warning messages from all files in the directory, or empty list if there was an error - * reading the directory or if there are no files in the directory - */ public static List> getExpectedWarningsFromDirectory(Path dirPath) { return getExpectedDiagnosticsFromDirectory(dirPath, "warning"); } @@ -129,11 +79,7 @@ private static List> getExpectedDiagnosticsFromDirectory(P return expectedDiagnostics; } - /** - * Helper method to add an integer variable to the context - */ public static void addIntVariableToContext(String name) { - context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), - factory.Code().createCodeSnippetStatement("")); + context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), factory.Code().createCodeSnippetStatement("")); } } From ffef6f5b5c10e67a1f51dd5ab71eb1388ea5185a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 12 Sep 2026 23:10:19 +0100 Subject: [PATCH 4/8] Improve Expected Pattern in Tests --- .../src/main/java/testSuite/ErrorAfterIf.java | 4 ++-- .../src/main/java/testSuite/ErrorAlias.java | 2 +- .../testSuite/ErrorAliasArgumentSize.java | 2 +- .../testSuite/ErrorAliasEmptyArguments.java | 2 +- .../java/testSuite/ErrorAliasNotFound.java | 2 +- .../main/java/testSuite/ErrorAliasSimple.java | 2 +- .../testSuite/ErrorAliasTypeMismatch.java | 2 +- .../ErrorArithmeticBinaryOperations.java | 2 +- .../java/testSuite/ErrorArithmeticFP.java | 8 ++++---- .../ErrorAssignementAfterDeclaration.java | 2 +- .../ErrorAssignmentBeforeReturn.java | 2 +- .../src/main/java/testSuite/ErrorBoolean.java | 2 +- .../testSuite/ErrorBooleanFunInvocation.java | 2 +- .../java/testSuite/ErrorBooleanLiteral.java | 2 +- .../main/java/testSuite/ErrorBoxedTypes.java | 6 +++--- .../src/main/java/testSuite/ErrorChars.java | 2 +- .../testSuite/ErrorDependentRefinement.java | 2 +- .../testSuite/ErrorDependentUpperBound.java | 2 +- .../ErrorDotNotationIncrementOnce.java | 2 +- .../testSuite/ErrorDotNotationMultiple.java | 2 +- .../ErrorDotNotationTrafficLight.java | 2 +- .../ErrorEnumFunctionRefinement.java | 2 +- .../java/testSuite/ErrorEnumNegation.java | 2 +- .../main/java/testSuite/ErrorEnumNull.java | 2 +- .../main/java/testSuite/ErrorEnumUsage.java | 2 +- .../main/java/testSuite/ErrorExtraToken.java | 2 +- .../testSuite/ErrorFunctionDeclarations.java | 2 +- .../testSuite/ErrorFunctionInvocation.java | 6 +++--- .../java/testSuite/ErrorGhostArgsTypes.java | 2 +- .../java/testSuite/ErrorGhostNotFound.java | 2 +- .../java/testSuite/ErrorGhostNumberArgs.java | 2 +- .../main/java/testSuite/ErrorIdentity.java | 2 +- .../java/testSuite/ErrorIfAssignment.java | 4 ++-- .../testSuite/ErrorImageWriteParamModes.java | 2 +- ...rrorImplementationSearchValueIntArray.java | 2 +- .../ErrorInstanceVarInRefinement.java | 4 ++-- .../java/testSuite/ErrorIntegerDivision.java | 2 +- .../testSuite/ErrorInvalidRefinement.java | 6 +++--- .../testSuite/ErrorIteratorReturnHasNext.java | 6 +++--- .../java/testSuite/ErrorLenZeroIntArray.java | 2 +- .../main/java/testSuite/ErrorLiteralZero.java | 2 +- .../main/java/testSuite/ErrorLongUsage.java | 4 ++-- .../testSuite/ErrorLongUsagePredicates.java | 6 +++--- .../ErrorMissingAliasTypeParameter.java | 2 +- .../testSuite/ErrorNoRefinementsInVar.java | 2 +- .../testSuite/ErrorOperatorAssignments.java | 12 +++++------ .../main/java/testSuite/ErrorRecursion.java | 2 +- .../testSuite/ErrorRecursiveDecrement.java | 2 +- .../ErrorRecursiveSiblingParameter.java | 4 ++-- .../java/testSuite/ErrorSearchIntArray.java | 2 +- .../testSuite/ErrorSearchValueIntArray.java | 4 ++-- .../java/testSuite/ErrorSimpleAssignment.java | 2 +- .../ErrorSourceStaticFinalInPredicate.java | 2 +- .../testSuite/ErrorSpecificArithmetic.java | 2 +- .../java/testSuite/ErrorSpecificValuesIf.java | 4 ++-- .../ErrorStaticFinalCharInPredicate.java | 2 +- .../testSuite/ErrorStaticFinalConstant.java | 2 +- .../ErrorStaticFinalInPredicate.java | 2 +- .../java/testSuite/ErrorSyntaxRefinement.java | 2 +- .../testSuite/ErrorSyntaxStateRefinement.java | 2 +- .../testSuite/ErrorTernaryExpression.java | 2 +- .../java/testSuite/ErrorTrafficLightRGB.java | 2 +- .../testSuite/ErrorTypeInRefinements.java | 2 +- .../java/testSuite/ErrorUnaryOperators.java | 4 ++-- .../ErrorUnconstrainedRefinement.java | 2 +- .../ErrorUnconstrainedStateRefinement.java | 2 +- .../ErrorWarningUnsatRefinement.java | 18 ++++++++--------- .../WarningExtRefNonExistentClass.java | 2 +- .../WarningExtRefNonExistentMethod.java | 2 +- .../WarningExtRefWrongConstructor.java | 2 +- .../WarningExtRefWrongParameterType.java | 2 +- .../testSuite/WarningExtRefWrongRetType.java | 2 +- .../testSuite/classes/ErrorGhostState.java | 2 +- .../boolean_ghost_error/SimpleTest.java | 2 +- .../classes/bytebuf_error/ByteBufTest.java | 4 ++-- .../SimpleTest.java | 2 +- .../SimpleTest.java | 2 +- .../classes/email_error/TestEmail.java | 2 +- .../image_params_so_error/JpegExporter.java | 4 ++-- .../index_out_of_bounds_error/Test.java | 2 +- .../classes/input_reader_error/Test.java | 2 +- .../classes/input_reader_error2/Test.java | 2 +- .../classes/iterator_error/Test.java | 2 +- .../iterator_interface_error/Test.java | 2 +- .../IteratorMisuse.java | 14 ++++++------- .../IteratorRemoveBeforeNext.java | 2 +- .../TestMethodOverloadEror.java | 2 +- .../ClassNoImport.java | 2 +- .../classes/order_gift_error/SimpleTest.java | 2 +- .../overload_constructors_error/Test.java | 2 +- .../refs_from_interface_error/SimpleTest.java | 2 +- .../SimpleTest.java | 2 +- .../ResultSetTests.java | 4 ++-- .../ResultSetTests.java | 10 +++++----- .../classes/scoreboard_error/SimpleTest.java | 2 +- .../testSuite/classes/socket_error/Test.java | 2 +- .../InputStreamReaderRefinements.java | 2 +- .../state_test_method_error/EditMisuse.java | 20 +++++++++---------- .../ts_bufferedreader_error/ConfigLoader.java | 4 ++-- .../field_updates/ErrorFieldUpdate.java | 2 +- .../java/testSuite/math/errorAbs/MathAbs.java | 2 +- .../java/testSuite/math/errorMax/MathMax.java | 2 +- .../errorMultiplyExact/MathMultiplyExact.java | 2 +- .../test/java/liquidjava/utils/TestUtils.java | 3 ++- 104 files changed, 162 insertions(+), 161 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java index f4cca99c0..29b0170ea 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java @@ -15,7 +15,7 @@ public void afterIf1(int a, int b) { pos = b; } @Refinement("_ == a || _ == b") - int r = pos; // Refinement Error + int r = pos; // Expect: Refinement Error } public void afterIf2() { @@ -26,6 +26,6 @@ public void afterIf2() { } k = 50; @Refinement("_ < 10") - int m = k; // Refinement Error + int m = k; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java index 90080d8c2..ec267f5dd 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java @@ -14,6 +14,6 @@ public static int getNum() { public static void main(String[] args) { @Refinement("InRange( _, 10, 15)") - int j = getNum(); // Refinement Error + int j = getNum(); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java index 030d3d448..db8f2fd11 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java @@ -8,7 +8,7 @@ public class ErrorAliasArgumentSize { public static void main(String[] args) { - @Refinement("InRange(j, 10)") // Argument Mismatch Error + @Refinement("InRange(j, 10)") // Expect: Argument Mismatch Error int j = 15; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java index a6e01718b..deef3d564 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java @@ -8,7 +8,7 @@ public class ErrorAliasEmptyArguments { public static void main(String[] args) { - @Refinement("InRange()") // Argument Mismatch Error + @Refinement("InRange()") // Expect: Argument Mismatch Error int j = 15; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java index e9da55860..3eb3c9e50 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java @@ -5,7 +5,7 @@ public class ErrorAliasNotFound { public static void main(String[] args) { - @Refinement("UndefinedAlias(x)") // Not Found Error + @Refinement("UndefinedAlias(x)") // Expect: Not Found Error int x = 5; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java index ea4c110cd..20b4ec343 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java @@ -9,6 +9,6 @@ public class ErrorAliasSimple { public static void main(String[] args) { @Refinement("PtGrade(_)") - double positiveGrade2 = 20 * 0.5 + 20 * 0.6; // Refinement Error + double positiveGrade2 = 20 * 0.5 + 20 * 0.6; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java index 037000bbc..7c9cda5a9 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java @@ -12,7 +12,7 @@ public static void main(String[] args) { @Refinement("PtGrade(_)") double positiveGrade2 = 20 * 0.5 + 20 * 0.5; - @Refinement("Positive(_)") // Argument Mismatch Error + @Refinement("Positive(_)") // Expect: Argument Mismatch Error double positive = positiveGrade2; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java index d0a892a93..15808bbd3 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java @@ -8,6 +8,6 @@ public static void main(String[] args) { @Refinement("_ < 100") int y = 50; @Refinement("_ > 0") - int z = y - 51; // Refinement Error + int z = y - 51; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java index 1ee5fc28e..266eafa54 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java @@ -7,7 +7,7 @@ public class ErrorArithmeticFP { private static void arithmetic1() { @Refinement("_ > 5.0") - double a = 5.0; // Refinement Error + double a = 5.0; // Expect: Refinement Error } private static void arithmetic2() { @@ -15,7 +15,7 @@ private static void arithmetic2() { double a = 5.5; @Refinement("_ == 10.0") - double c = a * 2.0; // Refinement Error + double c = a * 2.0; // Expect: Refinement Error } private static void arithmetic3() { @@ -23,7 +23,7 @@ private static void arithmetic3() { double a = 5.5; @Refinement("_ < -5.5") - double d = -a; // Refinement Error + double d = -a; // Expect: Refinement Error } private static void arithmetic4() { @@ -31,6 +31,6 @@ private static void arithmetic4() { double a = 5.5; @Refinement("_ < -5.5") - double d = -(a - 2.0); // Refinement Error + double d = -(a - 2.0); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java index e0c6b9405..079eb2565 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java @@ -12,6 +12,6 @@ public static void main(String[] args) { u = 11 + z; u = z * 2; u = 30 + z; - u = 500; // Refinement Error + u = 500; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java b/liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java index de75f2c72..862f179eb 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java @@ -6,6 +6,6 @@ public class ErrorAssignmentBeforeReturn { @Refinement("_ > 0") static int example(int x) { x = x + 1; - return x; // Refinement Error + return x; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java index 486ab222d..51c3fca6c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java @@ -6,6 +6,6 @@ public class ErrorBoolean { @Refinement("_ == true") boolean mustBeTrue(boolean value) { - return value; // Refinement Error + return value; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java index 726ff2b9a..9e7be868c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java @@ -21,6 +21,6 @@ public static void main(String[] args) { boolean o = !(a == 12); @Refinement("_ == true") - boolean m = greaterThanTen(a); // Refinement Error + boolean m = greaterThanTen(a); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java index 1147e6dde..c2468b274 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java @@ -12,6 +12,6 @@ public static void main(String[] args) { boolean k = (a < 11); @Refinement("_ == false") - boolean t = !(a == 12); // Refinement Error + boolean t = !(a == 12); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java index ddf42dcb9..a938159da 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java @@ -6,16 +6,16 @@ public class ErrorBoxedTypes { public static void errorBoxedBoolean() { @Refinement("_ == true") - Boolean b = false; // Refinement Error + Boolean b = false; // Expect: Refinement Error } public static void errorBoxedInteger() { @Refinement("_ > 0") - Integer j = -1; // Refinement Error + Integer j = -1; // Expect: Refinement Error } public static void errorBoxedDouble() { @Refinement("_ > 0") - Double d = -1.0; // Refinement Error + Double d = -1.0; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorChars.java b/liquidjava-example/src/main/java/testSuite/ErrorChars.java index dc4a04dde..771b83447 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorChars.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorChars.java @@ -8,6 +8,6 @@ static void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") } public static void main(String[] args) { - printLetter('$'); // Refinement Error + printLetter('$'); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java index d593bc629..b7cebfea1 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java @@ -10,6 +10,6 @@ public static void main(String[] args) { @Refinement("bigger > 20") int bigger = 50; @Refinement("_ > smaller && _ < bigger") - int middle = 21; // Refinement Error + int middle = 21; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java index 0310089a1..ad40b5a7b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java @@ -8,6 +8,6 @@ public class ErrorDependentUpperBound { int nextIndex( @Refinement("_ > 0") int len, @Refinement("0 <= _ && _ < len") int i) { - return i + 1; // Refinement Error + return i + 1; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java index 576fc86d3..aa23ecb3b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java @@ -15,6 +15,6 @@ public void incrementOnce() {} public static void main(String[] args) { ErrorDotNotationIncrementOnce t = new ErrorDotNotationIncrementOnce(); t.incrementOnce(); - t.incrementOnce(); // State Refinement Error + t.incrementOnce(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java index 6404d9aef..25df6814b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java @@ -12,7 +12,7 @@ public ErrorDotNotationMultiple() { } public static void main(String[] args) { - @Refinement("_ == this.not.size()") // Syntax Error + @Refinement("_ == this.not.size()") // Expect: Syntax Error int x = 0; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java index e1e8e076b..7ce92daf5 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java @@ -21,7 +21,7 @@ public void transitionToRed() {} public static void main(String[] args) { ErrorDotNotationTrafficLight tl = new ErrorDotNotationTrafficLight(); tl.transitionToAmber(); - tl.transitionToGreen(); // State Refinement Error + tl.transitionToGreen(); // Expect: State Refinement Error tl.transitionToRed(); } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java index aba1e1656..dca2162b5 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java @@ -18,6 +18,6 @@ Color changeColor(@Refinement("newColor == Color.Red || newColor == Color.Green" public static void main(String[] args) { ErrorEnumFunctionRefinement e = new ErrorEnumFunctionRefinement(); e.changeColor(Color.Red); - e.changeColor(Color.Blue); // Refinement Error + e.changeColor(Color.Blue); // Expect: Refinement Error } } \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java index 30d256da4..63b2fa7fb 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java @@ -13,6 +13,6 @@ void process(@Refinement("status != Status.Inactive") Status status) {} public static void main(String[] args) { ErrorEnumNegation e = new ErrorEnumNegation(); e.process(Status.Active); - e.process(Status.Inactive); // Refinement Error + e.process(Status.Inactive); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java index 400aa301b..a7f1b4d85 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java @@ -10,6 +10,6 @@ enum Color { public static void main(String[] args) { @Refinement("c == Color.Red || c == Color.Green") - Color c = null; // Refinement Error + Color c = null; // Expect: Refinement Error } } \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java index d4e98804c..a35b5a4c6 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java @@ -28,6 +28,6 @@ public static void main(String[] args) { // Correct ErrorEnumUsage st = new ErrorEnumUsage(); st.setMode(Mode.Video); - st.takePhoto(); // State Refinement Error + st.takePhoto(); // Expect: State Refinement Error } } \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java b/liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java index 9c5940659..55ae22be2 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorExtraToken.java @@ -6,7 +6,7 @@ public class ErrorExtraToken { void test() { - @Refinement("true false") // Syntax Error + @Refinement("true false") // Expect: Syntax Error int a = 1; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java index bca7d2598..3fdd18005 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java @@ -5,6 +5,6 @@ public class ErrorFunctionDeclarations { @Refinement("_ >= d && _ < i") private static int range(@Refinement("d >= 0") int d, @Refinement("i > d") int i) { - return i + 1; // Refinement Error + return i + 1; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java index e2f51f433..0218f181f 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java @@ -30,7 +30,7 @@ private static int getOne() { public static void invocation1() { @Refinement("_ > 10") - int p = 10; // Refinement Error + int p = 10; // Expect: Refinement Error p = posMult(10, 4); } @@ -40,12 +40,12 @@ public static void invocation2() { @Refinement("_ > 0") int c = getOne(); - c = getZero(); // Refinement Error + c = getZero(); // Expect: Refinement Error } public static void invocationWParams() { @Refinement("_ >= 0") int p = 10; - p = posMult(10, 12); // Refinement Error + p = posMult(10, 12); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java index d9a519674..6cc6dafa8 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java @@ -7,6 +7,6 @@ public class ErrorGhostArgsTypes { @Refinement("open(4.5) == true") public int one() { - return 1; // Argument Mismatch Error + return 1; // Expect: Argument Mismatch Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java index 49fd90ad0..50a26625e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java @@ -5,7 +5,7 @@ public class ErrorGhostNotFound { public static void main(String[] args) { - @Refinement("notFound(x)") // Not Found Error + @Refinement("notFound(x)") // Expect: Not Found Error int x = 5; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java index 2fd812d8d..8e47067bf 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java @@ -7,6 +7,6 @@ public class ErrorGhostNumberArgs { @Refinement("open(1,2) == true") public int one() { - return 1; // Argument Mismatch Error + return 1; // Expect: Argument Mismatch Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java b/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java index a88c80918..496997e05 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java @@ -6,6 +6,6 @@ public class ErrorIdentity { @Refinement("_ > 0") int positiveIdentity(int x) { - return x; // Refinement Error + return x; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java index ecaa52a27..d74bab86e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java @@ -12,7 +12,7 @@ public static void ifAssignment1() { @Refinement("b > 0") int b = a; b++; - a = 10; // Refinement Error + a = 10; // Expect: Refinement Error } } @@ -20,6 +20,6 @@ public static void ifAssignment2() { @Refinement("_ < 10") int a = 5; if (a < 0) - a = 100; // Refinement Error + a = 100; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorImageWriteParamModes.java b/liquidjava-example/src/main/java/testSuite/ErrorImageWriteParamModes.java index aecfff10d..e0d86fc41 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorImageWriteParamModes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorImageWriteParamModes.java @@ -12,6 +12,6 @@ static void requireExplicit(@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") in public static void main(String[] args) { // MODE_DEFAULT is 1, not 2 (MODE_EXPLICIT). - requireExplicit(ImageWriteParam.MODE_DEFAULT); // Refinement Error + requireExplicit(ImageWriteParam.MODE_DEFAULT); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java index 877105773..fddfef276 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java @@ -12,6 +12,6 @@ public static int getIndexWithValue( if (l[i] == val) return i; if (i >= l.length) // with or without -1 return -1; - else return getIndexWithValue(l, i + 1, val); // Refinement Error + else return getIndexWithValue(l, i + 1, val); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java index fdaa92a9c..4c0f6abe5 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java @@ -10,7 +10,7 @@ public static void varInRefinementInIf() { if (a > 0) { a = -2; @Refinement("b < a") - int b = -3; // Refinement Error + int b = -3; // Expect: Refinement Error } } @@ -19,6 +19,6 @@ public static void varInRefinement() { int a = 6; @Refinement("_ > a") - int b = 9; // Refinement Error + int b = 9; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java b/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java index 6f6e616c7..7f7f258cc 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java @@ -6,6 +6,6 @@ public class ErrorIntegerDivision { @Refinement("_ > 0") int half(@Refinement("_ > 0") int x) { - return x / 2; // Refinement Error + return x / 2; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java index 0f2853ac9..b0d570aa8 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java @@ -6,14 +6,14 @@ public class ErrorInvalidRefinement { void invalidRefinement() { - @Refinement("x") // Invalid Refinement Error + @Refinement("x") // Expect: Invalid Refinement Error int x = 0; } - void invalidRefinementParameter(@Refinement("y + 1") int y) { // Invalid Refinement Error + void invalidRefinementParameter(@Refinement("y + 1") int y) { // Expect: Invalid Refinement Error } - @Refinement("_ * 2") // Invalid Refinement Error + @Refinement("_ * 2") // Expect: Invalid Refinement Error void invalidRefinementReturn() { } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIteratorReturnHasNext.java b/liquidjava-example/src/main/java/testSuite/ErrorIteratorReturnHasNext.java index ea2196f24..a534fb77f 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIteratorReturnHasNext.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIteratorReturnHasNext.java @@ -30,13 +30,13 @@ void main1() { if(it.hasNext()){ it.next(); } else { - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } } void main2() { ErrorIteratorReturnHasNext it = new ErrorIteratorReturnHasNext(5); - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } int main3() { @@ -44,7 +44,7 @@ int main3() { int sum = 0; while (true){ if(!it.hasNext()){ - sum += it.next(); // State Refinement Error + sum += it.next(); // Expect: State Refinement Error } else { break; } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java index 9370fdd34..4e80cb32c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java @@ -13,6 +13,6 @@ public static int getIndexWithVal( public static void main(String[] args) { int[] a = new int[0]; - getIndexWithVal(a, 0, 6); // Refinement Error + getIndexWithVal(a, 0, 6); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java b/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java index 8490425ad..1297f8858 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java @@ -6,6 +6,6 @@ public class ErrorLiteralZero { @Refinement("_ != 0") int zero() { - return 0; // Refinement Error + return 0; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java index 524a9a02a..c90fbb8db 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java @@ -15,7 +15,7 @@ public static void longUsage1() { if (a > 5) { @Refinement("b < 50") - long b = a * 10; // Refinement Error + long b = a * 10; // Expect: Refinement Error } } @@ -24,6 +24,6 @@ public static void longUsage2() { long a = 9L; @Refinement("c > 40") - long c = doubleBiggerThanTwenty(a * 2); // Refinement Error + long c = doubleBiggerThanTwenty(a * 2); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java index fef6a5899..14edb90c7 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java @@ -5,16 +5,16 @@ public class ErrorLongUsagePredicates { void errorLargeSubtraction() { @Refinement("v - 9007199254740992 == 2") - long v = 9007199254740993L; // Refinement Error + long v = 9007199254740993L; // Expect: Refinement Error } void errorUUID() { @Refinement("((v/4096) % 16) == 2") - long v = 0x01000000122341666L; // Refinement Error + long v = 0x01000000122341666L; // Expect: Refinement Error } void errorWrongSign() { @Refinement("v < 0") - long v = 42L; // Refinement Error + long v = 42L; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java index 7c76be118..7d99431f0 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java @@ -2,5 +2,5 @@ import liquidjava.specification.RefinementAlias; -@RefinementAlias("Positive(v) { v > 0 }") // Syntax Error +@RefinementAlias("Positive(v) { v > 0 }") // Expect: Syntax Error public class ErrorMissingAliasTypeParameter {} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java b/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java index 9c8bcc261..e3b44d4f7 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java @@ -7,6 +7,6 @@ public class ErrorNoRefinementsInVar { public static void main(String[] args) { int a = 11; @Refinement("b < 10") - int b = a; // Refinement Error + int b = a; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorOperatorAssignments.java b/liquidjava-example/src/main/java/testSuite/ErrorOperatorAssignments.java index 1d55d76a2..e3fc893ff 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorOperatorAssignments.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorOperatorAssignments.java @@ -20,41 +20,41 @@ int remainder(@Refinement("_ >= 0") int x) { int plusInvocation(@Refinement("_ >= 0") int x) { int y = 10; y += remainder(x); - return y; // Refinement Error + return y; // Expect: Refinement Error } @Refinement("_ == 10") int plusUnaryInvocation() { int y = 10; y += -one(); - return y; // Refinement Error + return y; // Expect: Refinement Error } @Refinement("_ == 12") int plusConditional(@Refinement("_ >= 0") int x) { int y = 10; y += x >= 0 ? one() : 2; - return y; // Refinement Error + return y; // Expect: Refinement Error } @Refinement("_ == 14") int plusBinaryExpression() { int y = 10; y += one() + 2; - return y; // Refinement Error + return y; // Expect: Refinement Error } @Refinement("_ == 10") int plusArrayRead(int[] values) { int y = 10; y += values[0]; - return y; // Refinement Error + return y; // Expect: Refinement Error } @Refinement("_ == 12") int plusCast() { int y = 10; y += (int) one(); - return y; // Refinement Error + return y; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursion.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursion.java index 56b7f4f86..2513321a5 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorRecursion.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursion.java @@ -9,6 +9,6 @@ public static int untilZero(@Refinement("k >= 0") int k) { if (k == 1) return 0; else - return untilZero(k - 1); // Refinement Error + return untilZero(k - 1); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java index a9477c971..b2e4cb96a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java @@ -5,6 +5,6 @@ public class ErrorRecursiveDecrement { public int f(@Refinement("_ > 0") int x) { - return f(x - 1); // Refinement Error + return f(x - 1); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursiveSiblingParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveSiblingParameter.java index 8e48a2fb4..af2c906f8 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorRecursiveSiblingParameter.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveSiblingParameter.java @@ -8,10 +8,10 @@ int fibonacci(@Refinement("_ > 0") int n) { if (n == 1) return 1; else - return fibonacci(n - 1) + fibonacci(n - 2); // Refinement Error + return fibonacci(n - 1) + fibonacci(n - 2); // Expect: Refinement Error } int factorial(@Refinement("_ > 0") int n) { - return n * factorial(n - 1); // Refinement Error + return n * factorial(n - 1); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java index 1d2fa151d..8ed418685 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java @@ -7,6 +7,6 @@ public class ErrorSearchIntArray { public static void searchIndex( @Refinement("length(l) > 0") int[] l, @Refinement("i >= 0 && i <= length(l)") int i) { if (i > l.length) return; - else searchIndex(l, i + 1); // Refinement Error + else searchIndex(l, i + 1); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java index 3e0415f89..13c1a07fa 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java @@ -16,11 +16,11 @@ public static int getIndexWithValue( public static void searchValue1() { int[] arr = new int[10]; - getIndexWithValue(arr, arr.length, 1000); // Refinement Error + getIndexWithValue(arr, arr.length, 1000); // Expect: Refinement Error } public static void searchValue2(String[] args) { int[] arr = new int[0]; - getIndexWithValue(arr, 0, 1000); // Refinement Error + getIndexWithValue(arr, 0, 1000); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java index 2f8da6fde..eba87cf1b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java @@ -6,6 +6,6 @@ public class ErrorSimpleAssignment { public static void main(String[] args) { @Refinement("c > 2") - int c = 2; // Refinement Error + int c = 2; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSourceStaticFinalInPredicate.java b/liquidjava-example/src/main/java/testSuite/ErrorSourceStaticFinalInPredicate.java index 95e944a25..313f17017 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSourceStaticFinalInPredicate.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSourceStaticFinalInPredicate.java @@ -8,7 +8,7 @@ static void requireBelowLimit(@Refinement("_ < LIMITS.MAX") double x) { } public static void main(String[] args) { - requireBelowLimit(15.0); // Refinement Error + requireBelowLimit(15.0); // Expect: Refinement Error } static class LIMITS { diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java index 522ab27eb..296322ecd 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java @@ -12,6 +12,6 @@ public static void main(String[] args) { a = 6; b = a * 2; @Refinement("_ > 20") - int c = b * -1; // Refinement Error + int c = b * -1; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java index dd096788e..80f395754 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java @@ -16,7 +16,7 @@ public static void addZ(@Refinement("a > 0") int a) { int c = d; d = 10; @Refinement("b > 10") - int b = d; // Refinement Error + int b = d; // Expect: Refinement Error } } @@ -26,7 +26,7 @@ public static void addZ2() { if (a > 14) { a = 12; @Refinement("_ < 11") - int c = a; // Refinement Error + int c = a; // Expect: Refinement Error } } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalCharInPredicate.java b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalCharInPredicate.java index 26df3bbca..adfda5897 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalCharInPredicate.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalCharInPredicate.java @@ -8,6 +8,6 @@ static void requireMaxChar(@Refinement("_ == Character.MAX_VALUE") char c) { } public static void main(String[] args) { - requireMaxChar('\''); // Refinement Error + requireMaxChar('\''); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstant.java b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstant.java index b954e34e0..fa4889364 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstant.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstant.java @@ -9,6 +9,6 @@ static void requirePositive(@Refinement("_ > 0") int x) { } public static void main(String[] args) { - requirePositive(Integer.MIN_VALUE); // Refinement Error + requirePositive(Integer.MIN_VALUE); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java index 2e271b326..a40442c57 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java @@ -10,6 +10,6 @@ static void belowMaxByte(@Refinement("_ <= Byte.MAX_VALUE") int x) { public static void main(String[] args) { // Byte.MAX_VALUE == 127, so 200 violates the bound. - belowMaxByte(200); // Refinement Error + belowMaxByte(200); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java index 00f355024..e94ae9838 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java @@ -5,7 +5,7 @@ @SuppressWarnings("unused") public class ErrorSyntaxRefinement { public static void main(String[] args) { - @Refinement("_ < 100 +") // Syntax Error + @Refinement("_ < 100 +") // Expect: Syntax Error int value = 90 + 4; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java index 1fd29d49d..f13e07821 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java @@ -4,6 +4,6 @@ public class ErrorSyntaxStateRefinement { - @StateRefinement(from="$", to="#") // Syntax Error + @StateRefinement(from="$", to="#") // Expect: Syntax Error void test() {} } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java b/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java index b08b234bb..1fd639fb2 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java @@ -11,6 +11,6 @@ public static int three() { public static void main(String[] args) { @Refinement("_ < 10") int a = 5; - a = (a == 2) ? 6 + three() : 4 * three(); // Refinement Error + a = (a == 2) ? 6 + three() : 4 * three(); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java index e1b38235d..a56b6110d 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java @@ -48,6 +48,6 @@ public static void main(String[] args) { ErrorTrafficLightRGB tl = new ErrorTrafficLightRGB(); tl.transitionToAmber(); tl.transitionToRed(); - tl.transitionToAmber(); // State Refinement Error + tl.transitionToAmber(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java index 965a238f8..b30feede5 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java @@ -8,7 +8,7 @@ public class ErrorTypeInRefinements { public static void main(String[] args) { int a = 10; - @Refinement("(b == 6)") // Error + @Refinement("(b == 6)") // Expect: Error boolean b = true; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java index de8571568..b5539f2ee 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java @@ -10,12 +10,12 @@ public static void errorUnaryOperators() { v--; @Refinement("_ >= 10") int s = 10; - s--; // Refinement Error + s--; // Expect: Refinement Error } public static void errorUnaryOperatorMinus() { @Refinement("b > 0") int b = 8; - b = -b; // Refinement Error + b = -b; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedRefinement.java index 251c22bc3..7a068e52b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedRefinement.java @@ -7,6 +7,6 @@ public class ErrorUnconstrainedRefinement { private static void requirePositive(@Refinement("_ > 0") int value) {} public static void check(int value) { - requirePositive(value); // Refinement Error + requirePositive(value); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedStateRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedStateRefinement.java index 3fb4e0dc8..449281963 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedStateRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedStateRefinement.java @@ -10,6 +10,6 @@ public class ErrorUnconstrainedStateRefinement { public void run() {} public static void check(ErrorUnconstrainedStateRefinement value) { - value.run(); // State Refinement Error + value.run(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java index 98cd8092f..ea94559f1 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java @@ -5,24 +5,24 @@ public class ErrorWarningUnsatRefinement { public void example1() { - @Refinement("x == 1 && x != 1") // Unsat Refinement Warning - int x = 1; // Refinement Error + @Refinement("x == 1 && x != 1") // Expect: Unsat Refinement Warning + int x = 1; // Expect: Refinement Error } public void example2() { - @Refinement("x % 2 > 1") // Unsat Refinement Warning - int x = 5; // Refinement Error + @Refinement("x % 2 > 1") // Expect: Unsat Refinement Warning + int x = 5; // Expect: Refinement Error } public void example3() { - @Refinement("false") // Unsat Refinement Warning - int x = 0; // Refinement Error + @Refinement("false") // Expect: Unsat Refinement Warning + int x = 0; // Expect: Refinement Error } - public void example4(@Refinement("x > 0 && x < 0") int x) {} // Unsat Refinement Warning + public void example4(@Refinement("x > 0 && x < 0") int x) {} // Expect: Unsat Refinement Warning - @Refinement("_ == true && _ == false") // Unsat Refinement Warning + @Refinement("_ == true && _ == false") // Expect: Unsat Refinement Warning public boolean example5() { - return true; // Refinement Error + return true; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java index 6d0fd1fd1..f184d2637 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java @@ -2,7 +2,7 @@ import liquidjava.specification.ExternalRefinementsFor; -@ExternalRefinementsFor("non.existent.Class") // Warning +@ExternalRefinementsFor("non.existent.Class") // Expect: Warning public interface WarningExtRefNonExistentClass { public void NonExistentClass(); } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java index e1794c589..6f28bed8c 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java @@ -12,5 +12,5 @@ public interface WarningExtRefNonExistentMethod { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public boolean adddd(E e); // Warning + public boolean adddd(E e); // Expect: Warning } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java index 76b0a4c4b..3c9e551fc 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java @@ -9,7 +9,7 @@ public interface WarningExtRefWrongConstructor { @StateRefinement(to = "size(this) == 0") - public void ArrayList(String wrongParameter); // Warning + public void ArrayList(String wrongParameter); // Expect: Warning @StateRefinement(to = "size(this) == (size(old(this)) + 1)") public boolean add(E e); diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java index 5b31471b7..a10c4786b 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java @@ -12,5 +12,5 @@ public interface WarningExtRefWrongParameterType { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public boolean add(int wrongParameter); // Warning + public boolean add(int wrongParameter); // Expect: Warning } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java index 61994d53a..14da0792d 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java @@ -12,5 +12,5 @@ public interface WarningExtRefWrongRetType { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public int add(E e); // Warning + public int add(E e); // Expect: Warning } diff --git a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java index d042dd229..984f3bebf 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java +++ b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java @@ -5,7 +5,7 @@ import liquidjava.specification.StateSet; @StateSet({"empty", "addingItems", "checkout", "closed"}) -@Ghost("int totalPrice(int x)") // Error +@Ghost("int totalPrice(int x)") // Expect: Error public class ErrorGhostState { @StateRefinement(to = "(totalPrice(this) == 0) && empty(this)") diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java index 67cc3afd0..98c80205a 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java @@ -5,6 +5,6 @@ public static void main(String[] args) { SimpleStateMachine ssm = new SimpleStateMachine(); ssm.open(); ssm.close(); - ssm.execute(); // State Refinement Error + ssm.execute(); // Expect: State Refinement Error } } \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java index ca7f35f1e..645410b0b 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java @@ -17,12 +17,12 @@ public ByteBufTest() { mDirectBuffer = ByteBuffer.allocateDirect(TEST_BUFFER_SIZE); // VIOLATION: a direct buffer is not array-backed -> array() throws // UnsupportedOperationException. - byte[] buf = mDirectBuffer.array(); // State Refinement Error + byte[] buf = mDirectBuffer.array(); // Expect: State Refinement Error buf[1] = 100; } public void test(ByteBuffer mDirectBuffer) { - printBuffer("nativeInitDirectBuffer", mDirectBuffer.array()); // State Refinement Error + printBuffer("nativeInitDirectBuffer", mDirectBuffer.array()); // Expect: State Refinement Error } private void printBuffer(String tag, byte[] buffer) { diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/SimpleTest.java index 7dbb574a3..163fd8d13 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/SimpleTest.java @@ -5,6 +5,6 @@ public static void main(String[] args) { Downloader d = new Downloader(); d.start(); d.update(50); - d.update(40); // Refinement Error + d.update(40); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/SimpleTest.java index f38e46688..7e7a994c2 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/SimpleTest.java @@ -5,6 +5,6 @@ public static void main(String[] args) { Downloader d = new Downloader(); d.start(); d.update(50); - d.finish(); // State Refinement Error + d.finish(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/email_error/TestEmail.java b/liquidjava-example/src/main/java/testSuite/classes/email_error/TestEmail.java index 0cb56e6db..34f5e254c 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/email_error/TestEmail.java +++ b/liquidjava-example/src/main/java/testSuite/classes/email_error/TestEmail.java @@ -7,7 +7,7 @@ public static void main(String[] args) { Email e = new Email(); e.from("me"); // missing to - e.subject("not important"); // State Refinement Error + e.subject("not important"); // Expect: State Refinement Error e.body("body"); e.build(); } diff --git a/liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/JpegExporter.java b/liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/JpegExporter.java index a78e510bb..d5ada7f18 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/JpegExporter.java +++ b/liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/JpegExporter.java @@ -20,7 +20,7 @@ ImageWriteParam setCompressionPreferences() { ImageWriteParam param = new ImageWriteParam(Locale.getDefault()); if (param.canWriteCompressed()) { param.setCompressionMode(ImageWriteParam.MODE_DEFAULT); - param.setCompressionQuality(0.85f); // State Refinement Error + param.setCompressionQuality(0.85f); // Expect: State Refinement Error } return param; } @@ -37,7 +37,7 @@ public String compressImage(File multipartFile, RenderedImage image) throws IOEx writer.setOutput(ios); ImageWriteParam param = writer.getDefaultWriteParam(); - param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT); // State Refinement Error + param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT); // Expect: State Refinement Error param.setCompressionQuality(0.5f); writer.write(null, new IIOImage(image, null, null), param); diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java index 142cc7d8c..8c376f03e 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/Test.java @@ -5,6 +5,6 @@ public class Test { public static void main(String[] args) { ArrayList l = new ArrayList<>(); - l.get(0); // Refinement Error + l.get(0); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java index a65755e20..5ac8ff141 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java @@ -11,6 +11,6 @@ public static void main(String[] args) throws IOException { is.read(); is.read(); is.close(); - is.read(); // State Refinement Error + is.read(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/Test.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/Test.java index fd7b292ec..c331544ce 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/Test.java @@ -9,6 +9,6 @@ public static void main(String[] args) throws IOException { isr.read(); isr.close(); isr.getEncoding(); - isr.read(); // State Refinement Error + isr.read(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_error/Test.java index a418770db..23c07b250 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/iterator_error/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_error/Test.java @@ -5,6 +5,6 @@ public class Test { @SuppressWarnings("unused") public static void main(String[] args) { Iterator i = new Iterator(); - int x = i.next(true); // State Refinement Error + int x = i.next(true); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_interface_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_interface_error/Test.java index ceed8c72b..58f437eeb 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/iterator_interface_error/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_interface_error/Test.java @@ -9,6 +9,6 @@ public static void main(String[] args) { ArrayList list = new ArrayList<>(); list.add(new Object()); Iterator it = list.iterator(); - it.remove(); // State Refinement Error + it.remove(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java index 4aa1f52b1..cbfd71eff 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java @@ -6,21 +6,21 @@ public class IteratorMisuse { // No check at all: state of the parameter is unknown. public static void nextWithoutCheck(Scanner it) { - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } // Else branch of hasNext(): condition was false, so we know !hasMore. public static void nextInElseBranch(Scanner it) { if (it.hasNext()) { } else { - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } } // Negated check: !hasNext() true means hasNext returned false, so !hasMore. public static void nextNotInElse(Scanner it) { if (!it.hasNext()) { - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } } @@ -29,7 +29,7 @@ public static void nextNotInElse(Scanner it) { public static void doubleNextInThen(Scanner it) { if (it.hasNext()) { it.next(); - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } } @@ -38,7 +38,7 @@ public static void doubleNextInThen(Scanner it) { public static void nextAfterEmptyIf(Scanner it) { if (it.hasNext()) { } - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } // Sequential ifs: state is consumed by the first then-branch's next(), and the second if's @@ -49,7 +49,7 @@ public static void sequentialIfsLoseState(Scanner it) { } if (it.hasNext()) { } - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } // Empty if + empty else: neither branch establishes hasMore. @@ -57,6 +57,6 @@ public static void nextAfterEmptyIfElse(Scanner it) { if (it.hasNext()) { } else { } - it.next(); // State Refinement Error + it.next(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRemoveBeforeNext.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRemoveBeforeNext.java index c16c52e2c..30f792456 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRemoveBeforeNext.java +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRemoveBeforeNext.java @@ -37,7 +37,7 @@ public static void main(String[] args) { // VIOLATION: remove() before next() -> IllegalStateException // (NOT UnsupportedOperationException, so this catch does not fire). Iterator it = qev1.iterator(); - it.remove(); // State Refinement Error + it.remove(); // Expect: State Refinement Error } catch (UnsupportedOperationException e) { System.out.println("Calling Iterator.remove() and throwing exception."); } diff --git a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/TestMethodOverloadEror.java b/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/TestMethodOverloadEror.java index 7b912e374..22d583482 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/TestMethodOverloadEror.java +++ b/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/TestMethodOverloadEror.java @@ -5,6 +5,6 @@ public class TestMethodOverloadEror { public static void main(String[] args) throws InterruptedException { Semaphore sem = new Semaphore(1); - sem.acquire(-1); // Refinement Error + sem.acquire(-1); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java b/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java index e7a8925ac..67ec0b5a1 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java +++ b/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java @@ -7,7 +7,7 @@ public class ClassNoImport { // No import for javax.imageio.ImageWriteParam in this file — the verifier // should suggest it because Helper.java already imports it. - static void requireExplicit(@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) { // Not Found Error + static void requireExplicit(@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) { // Expect: Not Found Error } public static void main(String[] args) { diff --git a/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/SimpleTest.java index ee29d9a62..8d1546683 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/SimpleTest.java @@ -8,6 +8,6 @@ public static void main(String[] args) throws IOException { Order o = new Order(); Order f = o.addItem("shirt", 60).getNewOrderPayThis().addItem("t", 6).addItem("t", 1); o.addGift(); - f.addItem("l", 1).addGift(); // State Refinement Error + f.addItem("l", 1).addGift(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java index 4b29294c5..40b0fff3f 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java @@ -10,7 +10,7 @@ void test3(){ void test4(){ Throwable originT = new Throwable(); Throwable t = new Throwable(originT); - t.initCause(null); // State Refinement Error + t.initCause(null); // Expect: State Refinement Error t.getCause(); } diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/SimpleTest.java index 77f2978ef..0f9aa9609 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/SimpleTest.java @@ -6,6 +6,6 @@ public class SimpleTest { public static void main(String[] args) throws IOException { Bus b = new Bus(); - b.setYear(1500); // Refinement Error + b.setYear(1500); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/SimpleTest.java index 9439ed023..7081e3dcf 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/SimpleTest.java @@ -6,6 +6,6 @@ public class SimpleTest { public static void main(String[] args) throws IOException { Bus b = new Bus(); - b.setYear(1400); // Refinement Error + b.setYear(1400); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java index 4e1312265..aed5dae13 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java @@ -24,7 +24,7 @@ int login(Connection con, String username, String password) throws SQLException con.prepareStatement("select typeid from users where username=? and password=?", ResultSet.TYPE_SCROLL_INSENSITIVE, ResultSet.CONCUR_READ_ONLY); ResultSet rs = pstat.executeQuery(); - rs.beforeFirst(); // State Refinement Error + rs.beforeFirst(); // Expect: State Refinement Error return typeID; } @@ -40,7 +40,7 @@ int login2(Connection con, String username, String password) throws SQLException while (rs.next()) { rowCount++; } - rs.beforeFirst(); // State Refinement Error + rs.beforeFirst(); // Expect: State Refinement Error if (rowCount >= 1) { while (rs.next()) { typeID = rs.getInt(1); diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java index 166c52756..2d11210f4 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java @@ -30,7 +30,7 @@ int login(Connection con, String username, String password) throws SQLException // con.prepareStatement(sql, ResultSet.TYPE_SCROLL_INSENSITIVE, // ResultSet.CONCUR_READ_ONLY); // or drop the rewind and read typeID inside the single forward pass. - rs.beforeFirst(); // State Refinement Error + rs.beforeFirst(); // Expect: State Refinement Error return typeID; } @@ -48,7 +48,7 @@ int login2(Connection con, String username, String password) throws SQLException } // VIOLATION: beforeFirst() scrolls backward, illegal on a TYPE_FORWARD_ONLY // result set -> SQLException: Result set type is TYPE_FORWARD_ONLY. - rs.beforeFirst(); // State Refinement Error + rs.beforeFirst(); // Expect: State Refinement Error if (rowCount >= 1) { while (rs.next()) { typeID = rs.getInt(1); @@ -64,7 +64,7 @@ float readAverage(Connection conn) throws SQLException { parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); // FIX (from accepted answer): parentMessage.next(); // VIOLATION: cursor is before the first row; getFloat() with no next(). - float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error + float avgsum = parentMessage.getFloat("IMPAVG"); // Expect: State Refinement Error return avgsum; } @@ -75,7 +75,7 @@ float readAverageStoredNoGuard(Connection conn) throws SQLException { Statement parentstmt = conn.createStatement(); ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); boolean b = parentMessage.next(); - float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error + float avgsum = parentMessage.getFloat("IMPAVG"); // Expect: State Refinement Error return avgsum; } @@ -88,7 +88,7 @@ float readAverageVarElse(Connection conn) throws SQLException { if (b) { avgsum = parentMessage.getFloat("IMPAVG"); } else { - avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error + avgsum = parentMessage.getFloat("IMPAVG"); // Expect: State Refinement Error } return avgsum; } diff --git a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java index 3bf8bac42..572d6ee94 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java @@ -5,7 +5,7 @@ public static void main(String[] args) { Scoreboard sb = new Scoreboard(); sb.inc(); sb.dec(); - sb.dec(); // State Refinement Error + sb.dec(); // Expect: State Refinement Error sb.finish(); } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/socket_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/socket_error/Test.java index 84e9a2d48..349527370 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/socket_error/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/socket_error/Test.java @@ -15,7 +15,7 @@ public static void main(String[] args) throws IOException { Socket socket = new Socket(); socket.bind(new InetSocketAddress(inetAddress, port)); // socket.connect(new InetSocketAddress(inetAddress, port)); - socket.sendUrgentData(90); // State Refinement Error + socket.sendUrgentData(90); // Expect: State Refinement Error socket.close(); } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/InputStreamReaderRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/InputStreamReaderRefinements.java index 3ca9bb8a4..e4e19c95b 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/InputStreamReaderRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/InputStreamReaderRefinements.java @@ -12,7 +12,7 @@ @StateSet({"alreadyRead", "nothingRead"}) public interface InputStreamReaderRefinements { - @StateRefinement(to = "open(this) && close(this)") // State Conflict Error + @StateRefinement(to = "open(this) && close(this)") // Expect: State Conflict Error public void InputStreamReader(InputStream in); @StateRefinement(from = "open(this)", to = "open(this) && alreadyRead(this)") diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java index 236437bfc..14dd55dbf 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java @@ -7,19 +7,19 @@ public class EditMisuse { public static void undoInElseBranch(AbstractUndoableEdit edit) { if (edit.canUndo()) { } else { - edit.undo(); // State Refinement Error + edit.undo(); // Expect: State Refinement Error } } public static void undoNotInElse(AbstractUndoableEdit edit) { if (!edit.canUndo()) { - edit.undo(); // State Refinement Error + edit.undo(); // Expect: State Refinement Error } } public static void wrongTesterForRedo(AbstractUndoableEdit edit) { if (edit.canUndo()) { - edit.redo(); // State Refinement Error + edit.redo(); // Expect: State Refinement Error } } @@ -29,7 +29,7 @@ public static void wrongTester2() { if (edit.canUndo()) { edit.undo(); } - edit.undo(); // State Refinement Error + edit.undo(); // Expect: State Refinement Error } // Two undos in the same then-branch: condition forces aliveDone for the first, but the second @@ -37,7 +37,7 @@ public static void wrongTester2() { public static void doubleUndoInThen(AbstractUndoableEdit edit) { if (edit.canUndo()) { edit.undo(); - edit.undo(); // State Refinement Error + edit.undo(); // Expect: State Refinement Error } } @@ -46,7 +46,7 @@ public static void doubleUndoInThen(AbstractUndoableEdit edit) { public static void nestedIfRedoFromAliveDone(AbstractUndoableEdit edit) { if (edit.canUndo()) { if (edit.canUndo()) { - edit.redo(); // State Refinement Error + edit.redo(); // Expect: State Refinement Error } } } @@ -62,13 +62,13 @@ public static void sequentialIfsLoseState() { } if (edit.canUndo()) { } - edit.undo(); // State Refinement Error + edit.undo(); // Expect: State Refinement Error } // Wrong direction: canRedo() implies aliveNotDone, so calling undo() in that branch is illegal. public static void undoGuardedByCanRedo(AbstractUndoableEdit edit) { if (edit.canRedo()) { - edit.undo(); // State Refinement Error + edit.undo(); // Expect: State Refinement Error } } @@ -78,7 +78,7 @@ public static void doubleRedoAfterUndo(AbstractUndoableEdit edit) { if (edit.canUndo()) { edit.undo(); edit.redo(); - edit.redo(); // State Refinement Error + edit.redo(); // Expect: State Refinement Error } } @@ -90,6 +90,6 @@ public static void redoAfterEmptyIfElse() { if (edit.canUndo()) { } else { } - edit.redo(); // State Refinement Error + edit.redo(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java index bc3f18100..12086b769 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java +++ b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java @@ -27,7 +27,7 @@ String loadFirstSetting(String configPath, String defaultValue) throws IOExcepti if (header.startsWith("#")) { // Header was a comment — the real value is on the next line. reader.close(); - return reader.readLine(); // State Refinement Error + return reader.readLine(); // Expect: State Refinement Error } reader.close(); @@ -42,7 +42,7 @@ String loadFirstSetting2(String configPath, String defaultValue) throws IOExcept reader.close(); // no return here } - reader.close(); // State Refinement Error + reader.close(); // Expect: State Refinement Error return header; } } 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 62527a784..a85657e96 100644 --- a/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java +++ b/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java @@ -12,6 +12,6 @@ public static void main(String[] args) { ErrorFieldUpdate t = new ErrorFieldUpdate(); t.n = -1; - t.shouldFailIfFieldIsNegative(); // State Refinement Error + t.shouldFailIfFieldIsNegative(); // Expect: State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/math/errorAbs/MathAbs.java b/liquidjava-example/src/main/java/testSuite/math/errorAbs/MathAbs.java index 5cd2f8ace..d2c5bc556 100644 --- a/liquidjava-example/src/main/java/testSuite/math/errorAbs/MathAbs.java +++ b/liquidjava-example/src/main/java/testSuite/math/errorAbs/MathAbs.java @@ -9,6 +9,6 @@ public static void main(String[] args) { int ab = Math.abs(-9); @Refinement("_ == 9") - int ab1 = -ab; // Refinement Error + int ab1 = -ab; // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMax/MathMax.java b/liquidjava-example/src/main/java/testSuite/math/errorMax/MathMax.java index 49f6d092d..46de4718a 100644 --- a/liquidjava-example/src/main/java/testSuite/math/errorMax/MathMax.java +++ b/liquidjava-example/src/main/java/testSuite/math/errorMax/MathMax.java @@ -9,6 +9,6 @@ public static void main(String[] args) { int ab = Math.abs(-9); @Refinement("_ == 9") - int ab1 = Math.max(-9, -ab); // Refinement Error + int ab1 = Math.max(-9, -ab); // Expect: Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathMultiplyExact.java b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathMultiplyExact.java index 72fd8e0d7..d827be98e 100644 --- a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathMultiplyExact.java +++ b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathMultiplyExact.java @@ -10,6 +10,6 @@ public static void main(String[] args) { @Refinement("_ == -mul") int mul1 = Math.multiplyExact(mul, -1); @Refinement("_ < 0") - int mul2 = Math.multiplyExact(mul1, mul1); // Refinement Error + int mul2 = Math.multiplyExact(mul1, mul1); // Expect: Refinement Error } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 33ee09b2f..145e2ae24 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -16,7 +16,8 @@ public class TestUtils { - private static final Pattern EXPECTED_DIAGNOSTIC = Pattern.compile("//\\s*(.*?\\b(Error|Warning)\\b)", Pattern.CASE_INSENSITIVE); + private static final Pattern EXPECTED_DIAGNOSTIC = Pattern.compile("//\\s*Expect:\\s*(.*?\\b(Error|Warning)\\b)", + Pattern.CASE_INSENSITIVE); private final static Factory factory = new Launcher().getFactory(); private final static Context context = Context.getInstance(); From 97a83d7fa15030b182c2d4cbafe981a1edbb1dc7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 12 Sep 2026 23:51:38 +0100 Subject: [PATCH 5/8] Diagnostic Based Test Results --- .../ResultSetTests.java | 4 +- .../math/errorAbs/MathRefinements.java | 12 ++-- .../math/errorMax/MathRefinements.java | 12 ++-- .../errorMultiplyExact/MathRefinements.java | 12 ++-- .../liquidjava/api/tests/TestExamples.java | 72 +++++++------------ .../test/java/liquidjava/utils/TestUtils.java | 15 +--- 6 files changed, 48 insertions(+), 79 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java index aed5dae13..0c6986432 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java @@ -24,7 +24,7 @@ int login(Connection con, String username, String password) throws SQLException con.prepareStatement("select typeid from users where username=? and password=?", ResultSet.TYPE_SCROLL_INSENSITIVE, ResultSet.CONCUR_READ_ONLY); ResultSet rs = pstat.executeQuery(); - rs.beforeFirst(); // Expect: State Refinement Error + rs.beforeFirst(); return typeID; } @@ -40,7 +40,7 @@ int login2(Connection con, String username, String password) throws SQLException while (rs.next()) { rowCount++; } - rs.beforeFirst(); // Expect: State Refinement Error + rs.beforeFirst(); if (rowCount >= 1) { while (rs.next()) { typeID = rs.getInt(1); diff --git a/liquidjava-example/src/main/java/testSuite/math/errorAbs/MathRefinements.java b/liquidjava-example/src/main/java/testSuite/math/errorAbs/MathRefinements.java index ce8bf6124..bf4787bef 100644 --- a/liquidjava-example/src/main/java/testSuite/math/errorAbs/MathRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/math/errorAbs/MathRefinements.java @@ -16,13 +16,13 @@ public interface MathRefinements { public int abs(int arg0); @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(long arg0); + public int abs(long arg0); // Expect: Warning @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(float arg0); + public int abs(float arg0); // Expect: Warning @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(double arg0); + public int abs(double arg0); // Expect: Warning @Refinement(" _ == a+b") public int addExact(int a, int b); @@ -43,13 +43,13 @@ public interface MathRefinements { public int decrementExact(int a); @Refinement("_ == (a-1)") - public int decrementExact(long a); + public int decrementExact(long a); // Expect: Warning @Refinement("_ == (a+1)") public int incrementExact(int a); @Refinement("_ == (a+1)") - public int incrementExact(long a); + public int incrementExact(long a); // Expect: Warning @Refinement("(a > b)? (_ == a):(_ == b)") public int max(int a, int b); @@ -58,7 +58,7 @@ public interface MathRefinements { public int min(int a, int b); @Refinement(" _ > 0.0 && _ < 1.0") - public long random(long a, long b); + public long random(long a, long b); // Expect: Warning @Refinement("((sig > 0)?(_ > 0):(_ < 0)) && (( _ == arg)||(_ == -arg))") public float copySign(float arg, float sig); diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMax/MathRefinements.java b/liquidjava-example/src/main/java/testSuite/math/errorMax/MathRefinements.java index 72a22f6e3..3b2c59d04 100644 --- a/liquidjava-example/src/main/java/testSuite/math/errorMax/MathRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/math/errorMax/MathRefinements.java @@ -16,13 +16,13 @@ public interface MathRefinements { public int abs(int arg0); @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(long arg0); + public int abs(long arg0); // Expect: Warning @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(float arg0); + public int abs(float arg0); // Expect: Warning @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(double arg0); + public int abs(double arg0); // Expect: Warning @Refinement(" _ == a+b") public int addExact(int a, int b); @@ -43,13 +43,13 @@ public interface MathRefinements { public int decrementExact(int a); @Refinement("_ == (a-1)") - public int decrementExact(long a); + public int decrementExact(long a); // Expect: Warning @Refinement("_ == (a+1)") public int incrementExact(int a); @Refinement("_ == (a+1)") - public int incrementExact(long a); + public int incrementExact(long a); // Expect: Warning @Refinement("(a > b)? (_ == a):(_ == b)") public int max(int a, int b); @@ -58,7 +58,7 @@ public interface MathRefinements { public int min(int a, int b); @Refinement(" _ > 0.0 && _ < 1.0") - public long random(long a, long b); + public long random(long a, long b); // Expect: Warning @Refinement("((sig > 0)?(_ > 0):(_ < 0)) && (( _ == arg)||(_ == -arg))") public float copySign(float arg, float sig); diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathRefinements.java b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathRefinements.java index 6d1281439..de7064b15 100644 --- a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathRefinements.java @@ -16,13 +16,13 @@ public interface MathRefinements { public int abs(int arg0); @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(long arg0); + public int abs(long arg0); // Expect: Warning @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(float arg0); + public int abs(float arg0); // Expect: Warning @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(double arg0); + public int abs(double arg0); // Expect: Warning @Refinement(" _ == a+b") public int addExact(int a, int b); @@ -43,13 +43,13 @@ public interface MathRefinements { public int decrementExact(int a); @Refinement("_ == (a-1)") - public int decrementExact(long a); + public int decrementExact(long a); // Expect: Warning @Refinement("_ == (a+1)") public int incrementExact(int a); @Refinement("_ == (a+1)") - public int incrementExact(long a); + public int incrementExact(long a); // Expect: Warning @Refinement("(a > b)? (_ == a):(_ == b)") public int max(int a, int b); @@ -58,7 +58,7 @@ public interface MathRefinements { public int min(int a, int b); @Refinement(" _ > 0.0 && _ < 1.0") - public long random(long a, long b); + public long random(long a, long b); // Expect: Warning @Refinement("((sig > 0)?(_ > 0):(_ < 0)) && (( _ == arg)||(_ == -arg))") public float copySign(float arg, float sig); 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 f088afbe6..791f68b57 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -8,6 +8,7 @@ import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; +import java.util.ArrayList; import java.util.Collection; import java.util.List; import java.util.stream.Stream; @@ -40,32 +41,11 @@ public void testPath(final Path path) { List> expectedWarnings = isDirectory ? getExpectedWarningsFromDirectory(path) : getExpectedWarningsFromFile(path); + List> expectedErrors = isDirectory ? getExpectedErrorsFromDirectory(path) + : getExpectedErrorsFromFile(path); - if (shouldWarn(pathName)) { - checkExpectedDiagnostics(pathName, diagnostics.getWarnings(), expectedWarnings, - diagnostics.getWarningOutput()); - } - - // verification should pass, check if any errors were found - if (shouldPass(pathName) && diagnostics.foundError()) { - System.out.println("Error in: " + pathName + " --- should pass but an error was found. \n" - + diagnostics.getErrorOutput()); - fail(); - } - // verification should fail, check if it failed as expected (multiple errors can be found) - else if (shouldFail(pathName)) { - if (!diagnostics.foundError()) { - System.out.println("Error in: " + pathName + " --- should fail but no errors were found. \n" - + diagnostics.getErrorOutput()); - fail(); - } else { - // check if expected error was found - List> expectedErrors = isDirectory ? getExpectedErrorsFromDirectory(path) - : getExpectedErrorsFromFile(path); - checkExpectedDiagnostics(pathName, diagnostics.getErrors(), expectedErrors, - diagnostics.getErrorOutput()); - } - } + checkExpectedDiagnostics(pathName, diagnostics.getErrors(), expectedErrors, diagnostics.getErrorOutput()); + checkExpectedDiagnostics(pathName, diagnostics.getWarnings(), expectedWarnings, diagnostics.getWarningOutput()); } /** @@ -78,19 +58,21 @@ private static void checkExpectedDiagnostics(String pathName, Collection> unmatched = new ArrayList<>(expected); for (LJDiagnostic diagnostic : found) { - boolean match = expected.stream().anyMatch(expectedDiagnostic -> matches(diagnostic, expectedDiagnostic)); - if (!match) { + int match = -1; + for (int i = 0; i < unmatched.size(); i++) { + if (matches(diagnostic, unmatched.get(i))) { + match = i; + break; + } + } + if (match < 0) { System.out.println( "Unexpected diagnostic in: " + pathName + " --- expected: " + expected + ". \n" + output); fail(); } + unmatched.remove(match); } } @@ -107,19 +89,16 @@ 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(); - // Files that start with "Correct", "Error" or "Warning" - boolean isFileStartingWithCorrectOrError = fileAttr.isRegularFile() - && (shouldPass(name) || shouldFail(name) || shouldWarn(name)); - - // Directories that contain "correct", "error" or "warning" - boolean isDirectoryWithCorrectOrError = fileAttr.isDirectory() - && (shouldPass(name) || shouldFail(name) || shouldWarn(name)); - - // Return true if either condition matches - return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError; + return (fileAttr.isRegularFile() || fileAttr.isDirectory()) && isTestPath(name); }); } + private static boolean isTestPath(String path) { + String lowerCasePath = path.toLowerCase(); + return lowerCasePath.contains("correct") || lowerCasePath.contains("error") + || lowerCasePath.contains("warning"); + } + /** * Verifies that multiple correct inputs can be processed together */ @@ -128,9 +107,10 @@ public void testMultiplePaths() { String[] paths = { "../liquidjava-example/src/main/java/testSuite/CorrectSimple.java", "../liquidjava-example/src/main/java/testSuite/classes/arraylist_correct", }; CommandLineLauncher.launch(paths); - // Check if any of the paths that should be correct found an error - if (diagnostics.foundError()) { - System.out.println("Error found in files that should be correct. \n" + diagnostics.getErrorOutput()); + // The inputs have no expected diagnostics. + if (diagnostics.foundError() || !diagnostics.getWarnings().isEmpty()) { + System.out.println( + "Unexpected diagnostic found. \n" + diagnostics.getErrorOutput() + diagnostics.getWarningOutput()); fail(); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 145e2ae24..6947e7ca7 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -21,18 +21,6 @@ public class TestUtils { private final static Factory factory = new Launcher().getFactory(); private final static Context context = Context.getInstance(); - public static boolean shouldPass(String path) { - return path.toLowerCase().contains("correct"); - } - - public static boolean shouldFail(String path) { - return path.toLowerCase().contains("error"); - } - - public static boolean shouldWarn(String path) { - return path.toLowerCase().contains("warning"); - } - public static List> getExpectedErrorsFromFile(Path filePath) { return getExpectedDiagnosticsFromFile(filePath, "error"); } @@ -81,6 +69,7 @@ private static List> getExpectedDiagnosticsFromDirectory(P } public static void addIntVariableToContext(String name) { - context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), factory.Code().createCodeSnippetStatement("")); + context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), + factory.Code().createCodeSnippetStatement("")); } } From a52ec32243acad3840c39c9b9fbdd6a8613529a1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 13 Sep 2026 00:02:03 +0100 Subject: [PATCH 6/8] Update README --- README.md | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 2318d02c8..823bc019d 100644 --- a/README.md +++ b/README.md @@ -111,19 +111,18 @@ This should output an error message describing the refinement violation. #### Testing -Run `mvn test` to run all the tests in LiquidJava. +Run `./mvnw test` to run all the tests in LiquidJava. -The starter test file is `TestExamples.java`, which runs the test suite under the `testSuite` directory in `liquidjava-example`. +The `TestExamples.java` test runs the Java files and test directories under the `testSuite` directory in `liquidjava-example`. -The test suite considers test cases: -1. Files that start with `Correct` or `Error` (e.g., `CorrectRecursion.java`) -2. Directories that contain the word `correct` or `error` (e.g., `arraylist_correct`) +Test results are determined by inline diagnostic expectations using comments: -Therefore, the files and folders that do not follow this pattern are ignored. +```java +value = -1; // Expect: Refinement Error +``` -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) +Each expected diagnostic must be reported, and every reported error or warning must have a corresponding expectation. +Tests with no expectation must produce no diagnostics. ## Project Structure From 20885c9d7bcd4685ef9ef7d1adae80a6b16f3160 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 13 Sep 2026 00:18:26 +0100 Subject: [PATCH 7/8] Improve Test Directory --- README.md | 4 ++++ .../liquidjava/api/tests/TestExamples.java | 19 ++++++++++--------- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 823bc019d..0ea95db62 100644 --- a/README.md +++ b/README.md @@ -115,6 +115,10 @@ Run `./mvnw test` to run all the tests in LiquidJava. The `TestExamples.java` test runs the Java files and test directories under the `testSuite` directory in `liquidjava-example`. +Test inputs are discovered as follows: +- Top-level Java files are treated as individual test inputs +- Leaf directories are treated as a single test input + Test results are determined by inline diagnostic expectations using comments: ```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 791f68b57..2dd58ee0a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -86,17 +86,18 @@ private static boolean matches(LJDiagnostic diagnostic, Pair ex * Returns the test suite paths to verify */ 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(); - return (fileAttr.isRegularFile() || fileAttr.isDirectory()) && isTestPath(name); - }); + Path testSuite = Paths.get("../liquidjava-example/src/main/java/testSuite/"); + return Files.find(testSuite, Integer.MAX_VALUE, + (path, attributes) -> attributes.isDirectory() ? isLeafDirectory(path) : attributes.isRegularFile() + && path.toString().endsWith(".java") && !isLeafDirectory(path.getParent())); } - private static boolean isTestPath(String path) { - String lowerCasePath = path.toLowerCase(); - return lowerCasePath.contains("correct") || lowerCasePath.contains("error") - || lowerCasePath.contains("warning"); + private static boolean isLeafDirectory(Path path) { + try (Stream children = Files.list(path)) { + return children.noneMatch(Files::isDirectory); + } catch (IOException e) { + return false; + } } /** From d8c7897ff75dd17c51ed47040e04b78f2ac202c2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 13 Sep 2026 00:28:38 +0100 Subject: [PATCH 8/8] Code Refactoring --- .../liquidjava/api/tests/TestExamples.java | 26 ++++++------------- .../test/java/liquidjava/utils/TestUtils.java | 9 +++++++ 2 files changed, 17 insertions(+), 18 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 2dd58ee0a..4abb162c3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -35,12 +35,11 @@ public class TestExamples { public void testPath(final Path path) { String pathName = path.getFileName().toString(); boolean isDirectory = Files.isDirectory(path); - - // run verification CommandLineLauncher.launch(path.toFile().toString()); List> expectedWarnings = isDirectory ? getExpectedWarningsFromDirectory(path) : getExpectedWarningsFromFile(path); + List> expectedErrors = isDirectory ? getExpectedErrorsFromDirectory(path) : getExpectedErrorsFromFile(path); @@ -54,8 +53,8 @@ public void testPath(final Path path) { private static void checkExpectedDiagnostics(String pathName, Collection found, List> expected, String output) { if (found.size() != expected.size()) { - System.out.println("Unexpected number of diagnostics found in: " + pathName + " --- expected exactly " - + expected.size() + ". \n" + output); + System.out.printf("Unexpected number of diagnostics found in: %s --- expected exactly %d.%n%s%n", pathName, + expected.size(), output); fail(); } List> unmatched = new ArrayList<>(expected); @@ -68,8 +67,7 @@ private static void checkExpectedDiagnostics(String pathName, Collection expected) { if (diagnostic.getPosition().getLine() != expected.second()) return false; + return !(diagnostic instanceof LJError) || diagnostic.getTitle().equals(expected.first()); } @@ -92,26 +91,17 @@ private static Stream sourcePaths() throws IOException { && path.toString().endsWith(".java") && !isLeafDirectory(path.getParent())); } - private static boolean isLeafDirectory(Path path) { - try (Stream children = Files.list(path)) { - return children.noneMatch(Files::isDirectory); - } catch (IOException e) { - return false; - } - } - /** * Verifies that multiple correct inputs can be processed together */ @Test public void testMultiplePaths() { String[] paths = { "../liquidjava-example/src/main/java/testSuite/CorrectSimple.java", - "../liquidjava-example/src/main/java/testSuite/classes/arraylist_correct", }; + "../liquidjava-example/src/main/java/testSuite/classes/arraylist_correct" }; CommandLineLauncher.launch(paths); - // The inputs have no expected diagnostics. if (diagnostics.foundError() || !diagnostics.getWarnings().isEmpty()) { - System.out.println( - "Unexpected diagnostic found. \n" + diagnostics.getErrorOutput() + diagnostics.getWarningOutput()); + System.out.printf("Unexpected diagnostic found.%n%s%s%n", diagnostics.getErrorOutput(), + diagnostics.getWarningOutput()); fail(); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 6947e7ca7..a3f381dbf 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -8,6 +8,7 @@ import java.util.List; import java.util.regex.Matcher; import java.util.regex.Pattern; +import java.util.stream.Stream; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; @@ -72,4 +73,12 @@ public static void addIntVariableToContext(String name) { context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), factory.Code().createCodeSnippetStatement("")); } + + public static boolean isLeafDirectory(Path path) { + try (Stream children = Files.list(path)) { + return children.noneMatch(Files::isDirectory); + } catch (IOException e) { + return false; + } + } }