From 232cb9a9224bfc0e01048a93d629c20648565288 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Fri, 13 Mar 2026 23:06:43 +0000 Subject: [PATCH 01/12] Changed test stacktrace printing Should now print the line of code throwing the error, as well as the error type and description. --- liquidjava-verifier/pom.xml | 3 +++ .../liquidjava/api/tests/TestExamples.java | 20 ++++++++++++------- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 07abf74f8..84ac29563 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -93,6 +93,9 @@ org.apache.maven.plugins maven-surefire-plugin 3.2.1 + + true + 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 0f3552e89..d1a8d561b 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -35,29 +35,35 @@ public void testPath(final Path path) { boolean isDirectory = Files.isDirectory(path); // run verification - CommandLineLauncher.launch(path.toAbsolutePath().toString()); + CommandLineLauncher.launch(path.toFile().toString()); // 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"); + 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 (we assume each error test has exactly one error) else if (shouldFail(pathName)) { if (!diagnostics.foundError()) { - System.out.println("Error in: " + pathName + " --- should fail but no errors were found"); + System.out.println("Error in: " + pathName + " --- should fail but no errors were found. \n" + + diagnostics.getErrorOutput()); fail(); } else { // check if expected error was found Optional expected = isDirectory ? getExpectedErrorFromDirectory(path) : getExpectedErrorFromFile(path); if (diagnostics.getErrors().size() > 1) { - System.out.println("Multiple errors found in: " + pathName + " --- expected exactly one error"); + System.out.println("Multiple errors found in: " + pathName + " --- expected exactly one error. \n" + + diagnostics.getErrorOutput()); + System.out.println(diagnostics.getErrorOutput()); fail(); } LJError error = diagnostics.getErrors().iterator().next(); if (error.getPosition() == null) { - System.out.println("Error in: " + pathName + " --- error has no position information"); + System.out.println("Error in: " + pathName + " --- error has no position information. \n" + + diagnostics.getErrorOutput()); + System.out.println(diagnostics.getErrorOutput()); fail(); } if (expected.isPresent()) { @@ -65,7 +71,7 @@ else if (shouldFail(pathName)) { String foundError = error.getTitle(); if (!foundError.equalsIgnoreCase(expectedError)) { System.out.println("Error in: " + pathName + " --- expected error: " + expectedError - + ", but found: " + foundError); + + ", but found: " + foundError + ". \n" + diagnostics.getErrorOutput()); fail(); } } else { @@ -115,7 +121,7 @@ public void testMultiplePaths() { 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"); + System.out.println("Error found in files that should be correct. \n" + diagnostics.getErrorOutput()); fail(); } } From a71772e16c6cada4aad70b0673b6c910dea949c4 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 14 Mar 2026 01:24:48 +0000 Subject: [PATCH 02/12] Modified test utils to allow inline errors Instead of using separate files or stating at the top of a class file the error that it should report, now it is read and all correctly defined errors are added to a list. It is then checked against the first error that occurred and reports back. Still only works with a single error reported, however. --- .../liquidjava/api/tests/TestExamples.java | 28 ++++----- .../test/java/liquidjava/utils/TestUtils.java | 61 ++++++++++++------- 2 files changed, 51 insertions(+), 38 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 d1a8d561b..eebea98e1 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -7,6 +7,7 @@ import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; +import java.util.List; import java.util.Optional; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; @@ -43,7 +44,7 @@ public void testPath(final Path path) { + diagnostics.getErrorOutput()); fail(); } - // verification should fail, check if it failed as expected (we assume each error test has exactly one error) + // 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" @@ -51,33 +52,30 @@ else if (shouldFail(pathName)) { fail(); } else { // check if expected error was found - Optional expected = isDirectory ? getExpectedErrorFromDirectory(path) - : getExpectedErrorFromFile(path); - if (diagnostics.getErrors().size() > 1) { - System.out.println("Multiple errors found in: " + pathName + " --- expected exactly one error. \n" - + diagnostics.getErrorOutput()); - System.out.println(diagnostics.getErrorOutput()); + List expected = isDirectory ? getExpectedErrorsFromDirectory(path) + : getExpectedErrorsFromFile(path); + if (diagnostics.getErrors().size() > expected.size()) { + System.out.println("Multiple errors found in: " + pathName + " --- expected exactly " + + expected.size() + " errors. \n" + diagnostics.getErrorOutput()); fail(); } LJError error = diagnostics.getErrors().iterator().next(); if (error.getPosition() == null) { System.out.println("Error in: " + pathName + " --- error has no position information. \n" + diagnostics.getErrorOutput()); - System.out.println(diagnostics.getErrorOutput()); fail(); } - if (expected.isPresent()) { - String expectedError = expected.get(); + if (!expected.isEmpty()) { String foundError = error.getTitle(); - if (!foundError.equalsIgnoreCase(expectedError)) { - System.out.println("Error in: " + pathName + " --- expected error: " + expectedError + if (!expected.contains(foundError)) { + System.out.println("Error in: " + pathName + " --- expected errors: " + expected + ", but found: " + foundError + ". \n" + diagnostics.getErrorOutput()); fail(); } } else { - System.out.println("No expected error message found for: " + pathName); - System.out.println("Please provide an expected error in " + (isDirectory - ? "a .expected file in the directory" : "the first line of the test file as a comment")); + System.out.println("No expected error messages found for: " + pathName); + System.out.println( + "Please provide the expected errors in the test file as comments starting with // at the end of the supposed error line."); fail(); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index cd15f869b..1a2b36c9c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -1,10 +1,11 @@ package liquidjava.utils; +import java.io.BufferedReader; import java.io.IOException; import java.nio.file.Files; import java.nio.file.Path; -import java.util.Optional; -import java.util.stream.Stream; +import java.util.ArrayList; +import java.util.List; public class TestUtils { @@ -27,41 +28,55 @@ public static boolean shouldFail(String path) { } /** - * Reads the expected error message from the first line of the given test file + * Reads the expected error messages from the given file by looking for a comment containing the expected error + * message. * * @param filePath * - * @return optional containing the expected error message if present, otherwise empty + * @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 Optional getExpectedErrorFromFile(Path filePath) { - try (Stream lines = Files.lines(filePath)) { - Optional first = lines.findFirst(); - if (first.isPresent() && first.get().startsWith("//")) { - return Optional.of(first.get().substring(2).trim()); - } else { - return Optional.empty(); + public static List getExpectedErrorsFromFile(Path filePath) { + List expectedErrors = new ArrayList<>(); + try (BufferedReader reader = Files.newBufferedReader(filePath)) { + String line; + while ((line = reader.readLine()) != null) { + int idx = line.indexOf("//"); + if (idx != -1 && line.substring(idx).contains("Error")) { + // only expects the error type, NOT the actual refinement error message, depends on deterministic + // variable names + String comment = line.substring(idx + 2).trim(); + int dotIdx = comment.indexOf(":"); + if (dotIdx != -1) { + comment = comment.substring(0, dotIdx).trim(); + } + expectedErrors.add(comment); + } } - } catch (Exception e) { - return Optional.empty(); + } catch (IOException e) { + return List.of(); } + return expectedErrors; } /** - * Reads the expected error message from a .expected file in the given directory + * Reads the expected error messages from all files in the given directory and combines them into a single list * * @param dirPath * - * @return optional containing the expected error message if present, otherwise empty + * @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 Optional getExpectedErrorFromDirectory(Path dirPath) { - Path expectedFilePath = dirPath.resolve(".expected"); - if (Files.exists(expectedFilePath)) { - try (Stream lines = Files.lines(expectedFilePath)) { - return lines.findFirst().map(String::trim); - } catch (IOException e) { - return Optional.empty(); + public static List getExpectedErrorsFromDirectory(Path dirPath) { + List expectedErrors = new ArrayList<>(); + try { + List files = Files.list(dirPath).filter(Files::isRegularFile).toList(); + for (Path file : files) { + getExpectedErrorsFromFile(file).forEach(expectedErrors::add); } + } catch (IOException e) { + return List.of(); } - return Optional.empty(); + return expectedErrors; } } From 46c131a71eee86d954c18fde52adf6616b9a389e Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 14 Mar 2026 12:08:51 +0000 Subject: [PATCH 03/12] Improved test error tracking Errors are now gathered with their line number and compared based on the message and position. Added a Pair record to --- .../liquidjava/api/tests/TestExamples.java | 31 ++++++++++++------- .../test/java/liquidjava/utils/TestUtils.java | 21 ++++++++++--- 2 files changed, 35 insertions(+), 17 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 eebea98e1..8bd31903f 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -1,6 +1,7 @@ package liquidjava.api.tests; import static liquidjava.utils.TestUtils.*; + import static org.junit.Assert.fail; import java.io.IOException; @@ -10,14 +11,19 @@ import java.util.List; import java.util.Optional; import java.util.stream.Stream; + import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; +import liquidjava.utils.TestUtils.Pair; + import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; +import liquidjava.diagnostics.ErrorPosition; + public class TestExamples { Diagnostics diagnostics = Diagnostics.getInstance(); @@ -52,25 +58,26 @@ else if (shouldFail(pathName)) { fail(); } else { // check if expected error was found - List expected = isDirectory ? getExpectedErrorsFromDirectory(path) + List expected = isDirectory ? getExpectedErrorsFromDirectory(path) : getExpectedErrorsFromFile(path); if (diagnostics.getErrors().size() > expected.size()) { System.out.println("Multiple errors found in: " + pathName + " --- expected exactly " + expected.size() + " errors. \n" + diagnostics.getErrorOutput()); fail(); } - LJError error = diagnostics.getErrors().iterator().next(); - if (error.getPosition() == null) { - System.out.println("Error in: " + pathName + " --- error has no position information. \n" - + diagnostics.getErrorOutput()); - fail(); - } if (!expected.isEmpty()) { - String foundError = error.getTitle(); - if (!expected.contains(foundError)) { - System.out.println("Error in: " + pathName + " --- expected errors: " + expected - + ", but found: " + foundError + ". \n" + diagnostics.getErrorOutput()); - fail(); + for (LJError e : diagnostics.getErrors()) { + String foundError = e.getTitle(); + int errorPosition = e.getPosition().lineStart(); + boolean match = expected.stream().anyMatch( + pair -> pair.errorMessage().equals(foundError) && pair.lineNumber() == errorPosition); + + if (!match) { + System.out.println("Error in: " + pathName + " --- expected errors: " + expected + + ", but found: " + foundError + " at " + errorPosition + ". \n" + + diagnostics.getErrorOutput()); + fail(); + } } } else { System.out.println("No expected error messages found for: " + pathName); diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 1a2b36c9c..d6d1f05c6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -8,6 +8,15 @@ import java.util.List; public class TestUtils { + /* + * A simple record to store an error message and its line number, used for expected errors read from test files + */ + public record Pair(String errorMessage, int lineNumber) { + @Override + public String toString() { + return errorMessage + " at " + lineNumber; + }; + } /** * Determines if the given path indicates that the test should pass @@ -36,11 +45,13 @@ public static boolean shouldFail(String path) { * @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) { - List expectedErrors = new ArrayList<>(); + public static List getExpectedErrorsFromFile(Path filePath) { + List expectedErrors = new ArrayList<>(); try (BufferedReader reader = Files.newBufferedReader(filePath)) { String line; + int lineNumber = 0; while ((line = reader.readLine()) != null) { + lineNumber++; int idx = line.indexOf("//"); if (idx != -1 && line.substring(idx).contains("Error")) { // only expects the error type, NOT the actual refinement error message, depends on deterministic @@ -50,7 +61,7 @@ public static List getExpectedErrorsFromFile(Path filePath) { if (dotIdx != -1) { comment = comment.substring(0, dotIdx).trim(); } - expectedErrors.add(comment); + expectedErrors.add(new Pair(comment, lineNumber)); } } } catch (IOException e) { @@ -67,8 +78,8 @@ public static List getExpectedErrorsFromFile(Path filePath) { * @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) { - List expectedErrors = new ArrayList<>(); + public static List getExpectedErrorsFromDirectory(Path dirPath) { + List expectedErrors = new ArrayList<>(); try { List files = Files.list(dirPath).filter(Files::isRegularFile).toList(); for (Path file : files) { From d83ec57705e61e67172dbd51c467efd85dddb875 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 14 Mar 2026 16:07:54 +0000 Subject: [PATCH 04/12] Refactored tests --- .../src/main/java/testSuite/CorrectBoxedTypes.java | 1 - liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java | 3 +-- .../src/main/java/testSuite/ErrorAfterIf2.java | 3 +-- liquidjava-example/src/main/java/testSuite/ErrorAlias.java | 3 +-- .../src/main/java/testSuite/ErrorAliasArgumentSize.java | 3 +-- .../src/main/java/testSuite/ErrorAliasEmptyArguments.java | 3 +-- .../src/main/java/testSuite/ErrorAliasNotFound.java | 3 +-- .../src/main/java/testSuite/ErrorAliasSimple.java | 3 +-- .../src/main/java/testSuite/ErrorAliasTypeMismatch.java | 3 +-- .../main/java/testSuite/ErrorArithmeticBinaryOperations.java | 3 +-- .../src/main/java/testSuite/ErrorArithmeticFP1.java | 3 +-- .../src/main/java/testSuite/ErrorArithmeticFP2.java | 3 +-- .../src/main/java/testSuite/ErrorArithmeticFP3.java | 3 +-- .../src/main/java/testSuite/ErrorArithmeticFP4.java | 3 +-- .../java/testSuite/ErrorAssignementAfterDeclaration.java | 3 +-- .../src/main/java/testSuite/ErrorBooleanFunInvocation.java | 3 +-- .../src/main/java/testSuite/ErrorBooleanLiteral.java | 3 +-- .../src/main/java/testSuite/ErrorBoxedBoolean.java | 3 +-- .../src/main/java/testSuite/ErrorBoxedDouble.java | 3 +-- .../src/main/java/testSuite/ErrorBoxedInteger.java | 3 +-- liquidjava-example/src/main/java/testSuite/ErrorChars.java | 3 +-- .../src/main/java/testSuite/ErrorDependentRefinement.java | 3 +-- .../main/java/testSuite/ErrorDotNotationIncrementOnce.java | 3 +-- .../src/main/java/testSuite/ErrorDotNotationMultiple.java | 3 +-- .../main/java/testSuite/ErrorDotNotationTrafficLight.java | 3 +-- .../src/main/java/testSuite/ErrorFunctionDeclarations.java | 3 +-- .../src/main/java/testSuite/ErrorFunctionInvocation.java | 3 +-- .../src/main/java/testSuite/ErrorFunctionInvocation1.java | 3 +-- .../main/java/testSuite/ErrorFunctionInvocationParams.java | 3 +-- .../src/main/java/testSuite/ErrorGhostArgsTypes.java | 3 +-- .../src/main/java/testSuite/ErrorGhostNotFound.java | 3 +-- .../src/main/java/testSuite/ErrorGhostNumberArgs.java | 3 +-- .../src/main/java/testSuite/ErrorIfAssignment.java | 3 +-- .../src/main/java/testSuite/ErrorIfAssignment2.java | 3 +-- .../testSuite/ErrorImplementationSearchValueIntArray.java | 3 +-- .../main/java/testSuite/ErrorInstanceVarInRefinement.java | 3 +-- .../main/java/testSuite/ErrorInstanceVarInRefinementIf.java | 3 +-- .../src/main/java/testSuite/ErrorInvalidRefinement.java | 3 +-- .../main/java/testSuite/ErrorInvalidRefinementParameter.java | 3 +-- .../main/java/testSuite/ErrorInvalidRefinementReturn.java | 3 +-- .../src/main/java/testSuite/ErrorLenZeroIntArray.java | 3 +-- .../src/main/java/testSuite/ErrorLongUsage1.java | 3 +-- .../src/main/java/testSuite/ErrorLongUsage2.java | 3 +-- .../src/main/java/testSuite/ErrorLongUsagePredicates1.java | 5 ++--- .../src/main/java/testSuite/ErrorLongUsagePredicates2.java | 5 ++--- .../src/main/java/testSuite/ErrorLongUsagePredicates3.java | 5 ++--- .../main/java/testSuite/ErrorMissingAliasTypeParameter.java | 3 +-- .../src/main/java/testSuite/ErrorNoRefinementsInVar.java | 3 +-- .../src/main/java/testSuite/ErrorRecursion1.java | 3 +-- .../src/main/java/testSuite/ErrorSearchIntArray.java | 3 +-- .../src/main/java/testSuite/ErrorSearchValueIntArray1.java | 3 +-- .../src/main/java/testSuite/ErrorSearchValueIntArray2.java | 3 +-- .../src/main/java/testSuite/ErrorSimpleAssignment.java | 3 +-- .../src/main/java/testSuite/ErrorSpecificArithmetic.java | 3 +-- .../src/main/java/testSuite/ErrorSpecificValuesIf.java | 3 +-- .../src/main/java/testSuite/ErrorSpecificValuesIf2.java | 3 +-- .../src/main/java/testSuite/ErrorSyntaxRefinement.java | 3 +-- .../src/main/java/testSuite/ErrorSyntaxStateRefinement.java | 3 +-- .../src/main/java/testSuite/ErrorTernaryExpression.java | 3 +-- .../src/main/java/testSuite/ErrorTrafficLightRGB.java | 3 +-- .../src/main/java/testSuite/ErrorTypeInRefinements.java | 3 +-- .../src/main/java/testSuite/ErrorUnaryOpMinus.java | 3 +-- .../src/main/java/testSuite/ErrorUnaryOperators.java | 3 +-- .../src/main/java/testSuite/classes/ErrorGhostState.java | 3 +-- .../java/testSuite/classes/boolean_ghost_error/.expected | 1 - .../testSuite/classes/boolean_ghost_error/SimpleTest.java | 2 +- .../src/main/java/testSuite/classes/email_error/.expected | 1 - .../main/java/testSuite/classes/email_error/TestEmail.java | 2 +- .../testSuite/classes/index_out_of_bounds_error/.expected | 1 - .../testSuite/classes/index_out_of_bounds_error/Test.java | 4 ++-- .../main/java/testSuite/classes/input_reader_error/.expected | 1 - .../main/java/testSuite/classes/input_reader_error/Test.java | 2 +- .../java/testSuite/classes/input_reader_error2/.expected | 1 - .../java/testSuite/classes/input_reader_error2/Test.java | 2 +- .../src/main/java/testSuite/classes/iterator_error/.expected | 1 - .../src/main/java/testSuite/classes/iterator_error/Test.java | 2 +- .../java/testSuite/classes/method_overload_error/.expected | 1 - .../method_overload_error/TestMethodOverloadEror.java | 4 ++-- .../main/java/testSuite/classes/order_gift_error/.expected | 1 - .../java/testSuite/classes/order_gift_error/SimpleTest.java | 2 +- .../testSuite/classes/refs_from_interface_error/.expected | 1 - .../classes/refs_from_interface_error/SimpleTest.java | 2 +- .../testSuite/classes/refs_from_superclass_error/.expected | 1 - .../classes/refs_from_superclass_error/SimpleTest.java | 2 +- .../main/java/testSuite/classes/scoreboard_error/.expected | 1 - .../java/testSuite/classes/scoreboard_error/SimpleTest.java | 4 ++-- .../src/main/java/testSuite/classes/socket_error/.expected | 1 - .../src/main/java/testSuite/classes/socket_error/Test.java | 2 +- .../java/testSuite/classes/state_multiple_error/.expected | 1 - .../state_multiple_error/InputStreamReaderRefinements.java | 2 +- .../main/java/testSuite/field_updates/ErrorFieldUpdate.java | 3 +-- .../src/main/java/testSuite/math/errorAbs/.expected | 1 - .../src/main/java/testSuite/math/errorAbs/MathAbs.java | 2 +- .../src/main/java/testSuite/math/errorMax/.expected | 1 - .../src/main/java/testSuite/math/errorMax/MathAbs.java | 2 +- .../main/java/testSuite/math/errorMultiplyExact/.expected | 1 - .../testSuite/math/errorMultiplyExact/MathMultiplyExact.java | 2 +- .../src/test/java/liquidjava/api/tests/TestExamples.java | 3 --- 98 files changed, 86 insertions(+), 170 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/email_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/math/errorMax/.expected delete mode 100644 liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected diff --git a/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java b/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java index 1a404775e..b79373adf 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java index fd375b097..592df70da 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -15,6 +14,6 @@ public void have2(int a, int b) { if (b > 0) pos = b; } @Refinement("_ == a || _ == b") - int r = pos; + int r = pos; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java index 3ae6ed8e3..3082a9899 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -13,6 +12,6 @@ public static void main(String[] args) { } k = 50; @Refinement("_ < 10") - int m = k; + int m = k; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java index 7ed258151..90080d8c2 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -15,6 +14,6 @@ public static int getNum() { public static void main(String[] args) { @Refinement("InRange( _, 10, 15)") - int j = getNum(); + int j = getNum(); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java index a5dd6c753..c01f2c215 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java @@ -1,4 +1,3 @@ -// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; @@ -10,6 +9,6 @@ public class ErrorAliasArgumentSize { public static void main(String[] args) { @Refinement("InRange(j, 10)") - int j = 15; + int j = 15; // Argument Mismatch Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java index 99231431d..a6e01718b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java @@ -1,4 +1,3 @@ -// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; @@ -9,7 +8,7 @@ public class ErrorAliasEmptyArguments { public static void main(String[] args) { - @Refinement("InRange()") + @Refinement("InRange()") // 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 ca21871ac..116c68f33 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java @@ -1,4 +1,3 @@ -// Not Found Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorAliasNotFound { public static void main(String[] args) { @Refinement("UndefinedAlias(x)") - int x = 5; + int x = 5; // Not Found Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java index 1e2f17875..8caa03c45 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -10,6 +9,6 @@ public class ErrorAliasSimple { public static void main(String[] args) { @Refinement("PtGrade(_)") - double positiveGrade2 = 20 * 0.5 + 20 * 0.6; + double positiveGrade2 = 20 * 0.5 + 20 * 0.6; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java index 263a0f9b7..0343401bd 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java @@ -1,4 +1,3 @@ -// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; @@ -14,6 +13,6 @@ public static void main(String[] args) { double positiveGrade2 = 20 * 0.5 + 20 * 0.5; @Refinement("Positive(_)") - double positive = positiveGrade2; + double positive = positiveGrade2; // Argument Mismatch Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java index b2add7fa1..d0a892a93 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -9,6 +8,6 @@ public static void main(String[] args) { @Refinement("_ < 100") int y = 50; @Refinement("_ > 0") - int z = y - 51; + int z = y - 51; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java index 45239bc66..83359da0f 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -8,6 +7,6 @@ public class ErrorArithmeticFP1 { public static void main(String[] args) { @Refinement("_ > 5.0") - double a = 5.0; + double a = 5.0; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java index 16e58df78..a3816b2e3 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -11,6 +10,6 @@ public static void main(String[] args) { double a = 5.5; @Refinement("_ == 10.0") - double c = a * 2.0; + double c = a * 2.0; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java index ae85bc500..ffeaf1a17 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -9,6 +8,6 @@ public static void main(String[] args) { @Refinement("_ > 5.0") double a = 5.5; @Refinement("_ < -5.5") - double d = -a; + double d = -a; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java index 88eed94ca..f7a105064 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -10,6 +9,6 @@ public static void main(String[] args) { double a = 5.5; @Refinement("_ < -5.5") - double d = -(a - 2.0); + double d = -(a - 2.0); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java index 60acfbd72..e0c6b9405 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -13,6 +12,6 @@ public static void main(String[] args) { u = 11 + z; u = z * 2; u = 30 + z; - u = 500; // error + u = 500; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java index 99cc67d6e..726ff2b9a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -22,6 +21,6 @@ public static void main(String[] args) { boolean o = !(a == 12); @Refinement("_ == true") - boolean m = greaterThanTen(a); + boolean m = greaterThanTen(a); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java index 09b97f7e1..1147e6dde 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -13,6 +12,6 @@ public static void main(String[] args) { boolean k = (a < 11); @Refinement("_ == false") - boolean t = !(a == 12); + boolean t = !(a == 12); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java index 93c6a3c12..acfaf4beb 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorBoxedBoolean { public static void main(String[] args) { @Refinement("_ == true") - Boolean b = false; + Boolean b = false; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java index 643b509ab..d51e1916f 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorBoxedDouble { public static void main(String[] args) { @Refinement("_ > 0") - Double d = -1.0; + Double d = -1.0; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java index 2d937e208..883569cde 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorBoxedInteger { public static void main(String[] args) { @Refinement("_ > 0") - Integer j = -1; + Integer j = -1; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorChars.java b/liquidjava-example/src/main/java/testSuite/ErrorChars.java index cbaf4b1d9..3fb517106 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorChars.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorChars.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -6,7 +5,7 @@ public class ErrorChars { void test() { - printLetter('$'); // error + printLetter('$'); // Refinement Error } void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) { diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java index 9c83af5ed..42f18673d 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -11,6 +10,6 @@ public static void main(String[] args) { @Refinement("bigger > 20") int bigger = 50; @Refinement("_ > smaller && _ < bigger") - int middle = 21; + int middle = 21; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java index 8bf065845..576fc86d3 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java @@ -1,4 +1,3 @@ -// State Refinement Error package testSuite; import liquidjava.specification.Ghost; @@ -16,6 +15,6 @@ public void incrementOnce() {} public static void main(String[] args) { ErrorDotNotationIncrementOnce t = new ErrorDotNotationIncrementOnce(); t.incrementOnce(); - t.incrementOnce(); // error + t.incrementOnce(); // State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java index 483309b3a..0fe943667 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java @@ -1,4 +1,3 @@ -// Syntax Error package testSuite; import liquidjava.specification.Ghost; @@ -12,7 +11,7 @@ public class ErrorDotNotationMultiple { public ErrorDotNotationMultiple() {} void test() { - @Refinement("_ == this.not.size()") + @Refinement("_ == this.not.size()") // 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 e40ddb306..e1e8e076b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java @@ -1,4 +1,3 @@ -// State Refinement Error package testSuite; import liquidjava.specification.StateRefinement; @@ -22,7 +21,7 @@ public void transitionToRed() {} public static void main(String[] args) { ErrorDotNotationTrafficLight tl = new ErrorDotNotationTrafficLight(); tl.transitionToAmber(); - tl.transitionToGreen(); // error + tl.transitionToGreen(); // State Refinement Error tl.transitionToRed(); } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java index e2184b677..bca7d2598 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -6,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; + return i + 1; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java index f1ca6bf7b..d7a03f16b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -14,7 +13,7 @@ public static int posMult(@Refinement("a == 10") int a, @Refinement("_ < a && _ public static void main(String[] args) { @Refinement("_ > 10") - int p = 10; + int p = 10; // Refinement Error p = posMult(10, 4); } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java index e4309a4c0..c83e4d2d0 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -28,6 +27,6 @@ public static void main(String[] args) { @Refinement("_ > 0") int c = getOne(); - c = getZero(); + c = getZero(); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java index 6d1fa4736..852a80150 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -15,6 +14,6 @@ public static int posMult(@Refinement("a == 10") int a, @Refinement("_ < a && _ public static void main(String[] args) { @Refinement("_ >= 0") int p = 10; - p = posMult(10, 12); + p = posMult(10, 12); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java index 6ff3be00a..d193ad7bd 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java @@ -1,4 +1,3 @@ -// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; @@ -8,6 +7,6 @@ public class ErrorGhostArgsTypes { @RefinementPredicate("ghost boolean open(int)") @Refinement("open(4.5) == true") public int one() { - return 1; + return 1; // Argument Mismatch Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java index be2af75cf..c56607b25 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java @@ -1,4 +1,3 @@ -// Not Found Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorGhostNotFound { public void test() { @Refinement("notFound(x)") - int x = 5; + int x = 5; // Not Found Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java index f9b8ef353..c29f83df6 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java @@ -1,4 +1,3 @@ -// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; @@ -9,6 +8,6 @@ public class ErrorGhostNumberArgs { @RefinementPredicate("ghost boolean open(int)") @Refinement("open(1,2) == true") public int one() { - return 1; + return 1; // Argument Mismatch Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java index 06c611264..426b7c3f7 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -13,7 +12,7 @@ public static void main(String[] args) { @Refinement("b > 0") int b = a; b++; - a = 10; + a = 10; // Refinement Error } } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java index 19692a5a9..ce67a6dc2 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorIfAssignment2 { public static void main(String[] args) { @Refinement("_ < 10") int a = 5; - if (a < 0) a = 100; + if (a < 0) a = 100; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java index 41061023f..9a26aeb59 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -13,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); + else return getIndexWithValue(l, i + 1, val); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java index 5edd96d8d..b62a0dd22 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -10,6 +9,6 @@ public static void main(String[] args) { int a = 6; @Refinement("_ > a") - int b = 9; + int b = 9; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java index f0a973fd9..43b41e88c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -11,7 +10,7 @@ public static void main(String[] args) { if (a > 0) { a = -2; @Refinement("b < a") - int b = -3; + int b = -3; // Refinement Error } } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java index 6933955fe..ff54ad612 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java @@ -1,4 +1,3 @@ -// Invalid Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -7,7 +6,7 @@ public class ErrorInvalidRefinement { void test() { - @Refinement("x") + @Refinement("x") // Invalid Refinement Error int x = 0; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java index c6a92e459..c7349fac0 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java @@ -1,11 +1,10 @@ -// Invalid Refinement Error package testSuite; import liquidjava.specification.Refinement; public class ErrorInvalidRefinementParameter { - void testInvalidRefinement(@Refinement("y + 1") int y) {} + void testInvalidRefinement(@Refinement("y + 1") int y) {} // Invalid Refinement Error int otherMethod() { return -1; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java index b106518b4..f4af39510 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java @@ -1,11 +1,10 @@ -// Invalid Refinement Error package testSuite; import liquidjava.specification.Refinement; public class ErrorInvalidRefinementReturn { - @Refinement("_ * 2") + @Refinement("_ * 2") // Invalid Refinement Error void test() { } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java index 2aadc6885..9370fdd34 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -14,6 +13,6 @@ public static int getIndexWithVal( public static void main(String[] args) { int[] a = new int[0]; - getIndexWithVal(a, 0, 6); + getIndexWithVal(a, 0, 6); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java index 2bc1d1f62..aa9b6d8e6 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -11,7 +10,7 @@ public static void main(String[] args) { if (a > 5) { @Refinement("b < 50") - long b = a * 10; + long b = a * 10; // Refinement Error } } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java index fe5a231ab..127434c31 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -16,6 +15,6 @@ public static void main(String[] args) { long a = 9L; @Refinement("c > 40") - long c = doubleBiggerThanTwenty(a * 2); + long c = doubleBiggerThanTwenty(a * 2); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java index 55504b0d2..93495c066 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -6,6 +5,6 @@ public class ErrorLongUsagePredicates1 { void testUUID(){ @Refinement("((v/4096) % 16) == 2") - long v = 0x01000000122341666L; + long v = 0x01000000122341666L; // Refinement Error } -} \ No newline at end of file +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java index fc760314f..7b6978ca4 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -6,6 +5,6 @@ public class ErrorLongUsagePredicates2 { void testLargeSubtractionWrong() { @Refinement("v - 9007199254740992 == 2") - long v = 9007199254740993L; + long v = 9007199254740993L; // Refinement Error } -} \ No newline at end of file +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java index e5412994a..d460abe78 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -6,6 +5,6 @@ public class ErrorLongUsagePredicates3 { void testWrongSign() { @Refinement("v < 0") - long v = 42L; + long v = 42L; // Refinement Error } -} \ No newline at end of file +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java index f53bf5582..7c76be118 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java @@ -1,7 +1,6 @@ -// Syntax Error package testSuite; import liquidjava.specification.RefinementAlias; -@RefinementAlias("Positive(v) { v > 0 }") +@RefinementAlias("Positive(v) { v > 0 }") // 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 c2133b272..9c8bcc261 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -8,6 +7,6 @@ public class ErrorNoRefinementsInVar { public static void main(String[] args) { int a = 11; @Refinement("b < 10") - int b = a; + int b = a; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java index 518d351ee..9ddc0e4ec 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -8,6 +7,6 @@ public class ErrorRecursion1 { @Refinement(" _ == 0") public static int untilZero(@Refinement("k >= 0") int k) { if (k == 1) return 0; - else return untilZero(k - 1); + else return untilZero(k - 1); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java index 54ac3507f..1d2fa151d 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -8,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); + else searchIndex(l, i + 1); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java index f7a968904..f7e4b0b9b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -17,6 +16,6 @@ public static int getIndexWithValue( public static void main(String[] args) { int[] arr = new int[0]; - getIndexWithValue(arr, 0, 1000); + getIndexWithValue(arr, 0, 1000); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java index 944b7e6f5..05c6360d8 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -17,6 +16,6 @@ public static int getIndexWithValue( public static void main(String[] args) { int[] arr = new int[10]; - getIndexWithValue(arr, arr.length, 1000); + getIndexWithValue(arr, arr.length, 1000); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java index d07f12592..2f8da6fde 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorSimpleAssignment { public static void main(String[] args) { @Refinement("c > 2") - int c = 2; // should emit error + int c = 2; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java index 65bdde9bc..522ab27eb 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -13,6 +12,6 @@ public static void main(String[] args) { a = 6; b = a * 2; @Refinement("_ > 20") - int c = b * -1; + int c = b * -1; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java index 04704a8e0..d44efc462 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -17,7 +16,7 @@ public static void addZ(@Refinement("a > 0") int a) { int c = d; d = 10; @Refinement("b > 10") - int b = d; + int b = d; // Refinement Error } } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java index 2cae544c5..1ec4ec329 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -11,7 +10,7 @@ public static void main(String[] args) { if (a > 14) { a = 12; @Refinement("_ < 11") - int c = a; + int c = a; // Refinement Error } } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java index b02c63d0a..00f355024 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java @@ -1,4 +1,3 @@ -// Syntax Error package testSuite; import liquidjava.specification.Refinement; @@ -6,7 +5,7 @@ @SuppressWarnings("unused") public class ErrorSyntaxRefinement { public static void main(String[] args) { - @Refinement("_ < 100 +") + @Refinement("_ < 100 +") // 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 14fd6a2ba..1fd29d49d 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java @@ -1,10 +1,9 @@ -// Syntax Error package testSuite; import liquidjava.specification.StateRefinement; public class ErrorSyntaxStateRefinement { - @StateRefinement(from="$", to="#") + @StateRefinement(from="$", to="#") // 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 2c89393ae..b08b234bb 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -12,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(); + a = (a == 2) ? 6 + three() : 4 * three(); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java index 3b50f6158..3f5d8eb9b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java @@ -1,4 +1,3 @@ -// State Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -49,6 +48,6 @@ public static void name() { ErrorTrafficLightRGB tl = new ErrorTrafficLightRGB(); tl.transitionToAmber(); tl.transitionToRed(); - tl.transitionToAmber(); + tl.transitionToAmber(); // State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java index 2981a2176..d2c5c8d3f 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java @@ -1,4 +1,3 @@ -// Error package testSuite; import liquidjava.specification.Refinement; @@ -10,6 +9,6 @@ public static void main(String[] args) { int a = 10; @Refinement("(b == 6)") - boolean b = true; + boolean b = true; // Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java index 73eb1529a..a4db398d9 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorUnaryOpMinus { public static void main(String[] args) { @Refinement("b > 0") int b = 8; - b = -b; + b = -b; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java index b8660ea83..f40a0e98e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -11,6 +10,6 @@ public static void main(String[] args) { v--; @Refinement("_ >= 10") int s = 10; - s--; + s--; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java index 80e2741c3..d042dd229 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java +++ b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java @@ -1,4 +1,3 @@ -// Error package testSuite.classes; import liquidjava.specification.Ghost; @@ -6,7 +5,7 @@ import liquidjava.specification.StateSet; @StateSet({"empty", "addingItems", "checkout", "closed"}) -@Ghost("int totalPrice(int x)") // Should have no parameters +@Ghost("int totalPrice(int x)") // Error public class ErrorGhostState { @StateRefinement(to = "(totalPrice(this) == 0) && empty(this)") diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected +++ /dev/null @@ -1 +0,0 @@ -State Refinement Error 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 7408096e7..67cc3afd0 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(); // error, not open + ssm.execute(); // State Refinement Error } } \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected +++ /dev/null @@ -1 +0,0 @@ -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 1756e6ea2..0cb56e6db 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"); + e.subject("not important"); // State Refinement Error e.body("body"); e.build(); } diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected deleted file mode 100644 index 6f476981c..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected +++ /dev/null @@ -1 +0,0 @@ -Refinement Error 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 eb61dfaea..142cc7d8c 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); // index out of bounds + l.get(0); // Refinement Error } -} \ No newline at end of file +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected +++ /dev/null @@ -1 +0,0 @@ -State 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 85d7dc672..a65755e20 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(); // should not be able to read + is.read(); // State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected +++ /dev/null @@ -1 +0,0 @@ -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 d3093679a..fd7b292ec 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(); + isr.read(); // State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected +++ /dev/null @@ -1 +0,0 @@ -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 9e039952f..a418770db 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); + int x = i.next(true); // State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected deleted file mode 100644 index 6f476981c..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected +++ /dev/null @@ -1 +0,0 @@ -Refinement Error 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 b977c1b0c..7b912e374 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); + sem.acquire(-1); // Refinement Error } -} \ No newline at end of file +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected +++ /dev/null @@ -1 +0,0 @@ -State Refinement Error 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 17a5d3c19..ee29d9a62 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(); + f.addItem("l", 1).addGift(); // State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected deleted file mode 100644 index 6f476981c..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected +++ /dev/null @@ -1 +0,0 @@ -Refinement Error 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 1bfc3694e..77f2978ef 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); + b.setYear(1500); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected deleted file mode 100644 index 6f476981c..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected +++ /dev/null @@ -1 +0,0 @@ -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 bf27a38e3..9439ed023 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); + b.setYear(1400); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected +++ /dev/null @@ -1 +0,0 @@ -State Refinement Error 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 0676175bb..3bf8bac42 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(); // error, underflow + sb.dec(); // State Refinement Error sb.finish(); } -} \ No newline at end of file +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected +++ /dev/null @@ -1 +0,0 @@ -State Refinement Error 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 cc2ebbf1f..84e9a2d48 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); + socket.sendUrgentData(90); // State Refinement Error socket.close(); } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected deleted file mode 100644 index 258d98bb8..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected +++ /dev/null @@ -1 +0,0 @@ -State Conflict Error 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 7d6b9a150..85c57be4a 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 @@ -13,7 +13,7 @@ public interface InputStreamReaderRefinements { @StateRefinement(to = "open(this) && close(this)") - public void InputStreamReader(InputStream in); + public void InputStreamReader(InputStream in); // State Conflict Error @StateRefinement(from = "open(this)", to = "open(this) && alreadyRead(this)") @Refinement("(_ >= -1) && (_ <= 127)") 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 55a101848..62527a784 100644 --- a/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java +++ b/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java @@ -1,4 +1,3 @@ -// State Refinement Error package testSuite.field_updates; import liquidjava.specification.StateRefinement; @@ -13,6 +12,6 @@ public static void main(String[] args) { ErrorFieldUpdate t = new ErrorFieldUpdate(); t.n = -1; - t.shouldFailIfFieldIsNegative(); + t.shouldFailIfFieldIsNegative(); // State Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected b/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected deleted file mode 100644 index 6f476981c..000000000 --- a/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected +++ /dev/null @@ -1 +0,0 @@ -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 e84275809..5cd2f8ace 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; + int ab1 = -ab; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected b/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected deleted file mode 100644 index 6f476981c..000000000 --- a/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected +++ /dev/null @@ -1 +0,0 @@ -Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMax/MathAbs.java b/liquidjava-example/src/main/java/testSuite/math/errorMax/MathAbs.java index 75c12d9ea..783fc469a 100644 --- a/liquidjava-example/src/main/java/testSuite/math/errorMax/MathAbs.java +++ b/liquidjava-example/src/main/java/testSuite/math/errorMax/MathAbs.java @@ -9,6 +9,6 @@ public static void main(String[] args) { int ab = Math.abs(-9); @Refinement("_ == 9") - int ab1 = -ab; + int ab1 = -ab; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected deleted file mode 100644 index 6f476981c..000000000 --- a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected +++ /dev/null @@ -1 +0,0 @@ -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 28f8d2cf4..72fd8e0d7 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); + int mul2 = Math.multiplyExact(mul1, mul1); // Refinement Error } } 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 8bd31903f..058ba205a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -9,7 +9,6 @@ import java.nio.file.Path; import java.nio.file.Paths; import java.util.List; -import java.util.Optional; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; @@ -22,8 +21,6 @@ import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; -import liquidjava.diagnostics.ErrorPosition; - public class TestExamples { Diagnostics diagnostics = Diagnostics.getInstance(); From 93dfe8f6238ea01efe7ac2f0c2edbfe92d4bf086 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 14 Mar 2026 20:28:18 +0000 Subject: [PATCH 05/12] Fixed changing method name --- .../testSuite/classes/overload_constructors_error/Test.java | 2 +- .../src/test/java/liquidjava/api/tests/TestExamples.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 407c23a3f..4b29294c5 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);// should be an error but its not + t.initCause(null); // State Refinement Error t.getCause(); } 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 058ba205a..dc1c285f4 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -65,7 +65,7 @@ else if (shouldFail(pathName)) { if (!expected.isEmpty()) { for (LJError e : diagnostics.getErrors()) { String foundError = e.getTitle(); - int errorPosition = e.getPosition().lineStart(); + int errorPosition = e.getPosition().getLine(); boolean match = expected.stream().anyMatch( pair -> pair.errorMessage().equals(foundError) && pair.lineNumber() == errorPosition); From 734d4963f94d623c1be2c3ebf7456b3dd5572965 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 14 Mar 2026 20:51:59 +0000 Subject: [PATCH 06/12] Applied suggested fixes Used existing Pairs, removing old code. Changed the way strings are matched via Regex. --- .../overload_constructors_error/.expected | 1 - .../liquidjava/api/tests/TestExamples.java | 18 +++++------ .../test/java/liquidjava/utils/TestUtils.java | 31 +++++++------------ 3 files changed, 20 insertions(+), 30 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected diff --git a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected deleted file mode 100644 index 49d2a05a3..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected +++ /dev/null @@ -1 +0,0 @@ -State Refinement Error 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 dc1c285f4..7c07d3c9c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -15,7 +15,7 @@ import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; -import liquidjava.utils.TestUtils.Pair; +import liquidjava.utils.Pair; import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; @@ -55,22 +55,22 @@ else if (shouldFail(pathName)) { fail(); } else { // check if expected error was found - List expected = isDirectory ? getExpectedErrorsFromDirectory(path) + List> expectedErrors = isDirectory ? getExpectedErrorsFromDirectory(path) : getExpectedErrorsFromFile(path); - if (diagnostics.getErrors().size() > expected.size()) { + if (diagnostics.getErrors().size() != expectedErrors.size()) { System.out.println("Multiple errors found in: " + pathName + " --- expected exactly " - + expected.size() + " errors. \n" + diagnostics.getErrorOutput()); + + expectedErrors.size() + " errors. \n" + diagnostics.getErrorOutput()); fail(); } - if (!expected.isEmpty()) { + if (!expectedErrors.isEmpty()) { for (LJError e : diagnostics.getErrors()) { String foundError = e.getTitle(); int errorPosition = e.getPosition().getLine(); - boolean match = expected.stream().anyMatch( - pair -> pair.errorMessage().equals(foundError) && pair.lineNumber() == errorPosition); + boolean match = expectedErrors.stream().anyMatch( + expected -> expected.first().equals(foundError) && expected.second() == errorPosition); if (!match) { - System.out.println("Error in: " + pathName + " --- expected errors: " + expected + System.out.println("Error in: " + pathName + " --- expected errors: " + expectedErrors + ", but found: " + foundError + " at " + errorPosition + ". \n" + diagnostics.getErrorOutput()); fail(); @@ -79,7 +79,7 @@ else if (shouldFail(pathName)) { } else { System.out.println("No expected error messages found for: " + pathName); System.out.println( - "Please provide the expected errors in the test file as comments starting with // at the end of the supposed error line."); + "Please specify each expected error in the test file as a comment on the line where the error should be reported."); fail(); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index d6d1f05c6..21a3b784e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -6,18 +6,10 @@ import java.nio.file.Path; import java.util.ArrayList; import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; public class TestUtils { - /* - * A simple record to store an error message and its line number, used for expected errors read from test files - */ - public record Pair(String errorMessage, int lineNumber) { - @Override - public String toString() { - return errorMessage + " at " + lineNumber; - }; - } - /** * Determines if the given path indicates that the test should pass * @@ -45,23 +37,22 @@ public static boolean shouldFail(String path) { * @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) { - List expectedErrors = new ArrayList<>(); + public static List> getExpectedErrorsFromFile(Path filePath) { + List> expectedErrors = new ArrayList<>(); try (BufferedReader reader = Files.newBufferedReader(filePath)) { String line; int lineNumber = 0; while ((line = reader.readLine()) != null) { lineNumber++; - int idx = line.indexOf("//"); - if (idx != -1 && line.substring(idx).contains("Error")) { - // only expects the error type, NOT the actual refinement error message, depends on deterministic - // variable names - String comment = line.substring(idx + 2).trim(); + Pattern p = Pattern.compile("//\\s*(.*?\\bError\\b)", Pattern.CASE_INSENSITIVE); + Matcher m = p.matcher(line); + if (m.find()) { + String comment = m.group(1).trim(); int dotIdx = comment.indexOf(":"); if (dotIdx != -1) { comment = comment.substring(0, dotIdx).trim(); } - expectedErrors.add(new Pair(comment, lineNumber)); + expectedErrors.add(new Pair<>(comment, lineNumber)); } } } catch (IOException e) { @@ -78,8 +69,8 @@ public static List getExpectedErrorsFromFile(Path filePath) { * @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) { - List expectedErrors = new ArrayList<>(); + public static List> getExpectedErrorsFromDirectory(Path dirPath) { + List> expectedErrors = new ArrayList<>(); try { List files = Files.list(dirPath).filter(Files::isRegularFile).toList(); for (Path file : files) { From 19e479cf3eb6ad50a541f80f6b866e4e65f1e88f Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sat, 14 Mar 2026 20:58:22 +0000 Subject: [PATCH 07/12] Removed unnecessary code --- .../src/test/java/liquidjava/utils/TestUtils.java | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 21a3b784e..10ac4d33d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -47,12 +47,7 @@ public static List> getExpectedErrorsFromFile(Path filePat Pattern p = Pattern.compile("//\\s*(.*?\\bError\\b)", Pattern.CASE_INSENSITIVE); Matcher m = p.matcher(line); if (m.find()) { - String comment = m.group(1).trim(); - int dotIdx = comment.indexOf(":"); - if (dotIdx != -1) { - comment = comment.substring(0, dotIdx).trim(); - } - expectedErrors.add(new Pair<>(comment, lineNumber)); + expectedErrors.add(new Pair<>(m.group(1).trim(), lineNumber)); } } } catch (IOException e) { From 51c0047a8d31e14b9758b10f85b891deda06b05f Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sun, 15 Mar 2026 20:13:51 +0000 Subject: [PATCH 08/12] Refactored tests Due to multiple error check/annotation, some tests have been merged into single files to reduce testing workload. Math tests need to be reviewed due to weird behavior if the refinements aren't alone in the same folder as the test. --- .../src/main/java/testSuite/ErrorAfterIf.java | 16 +++++++-- .../main/java/testSuite/ErrorAfterIf2.java | 17 --------- .../java/testSuite/ErrorArithmeticFP.java | 36 +++++++++++++++++++ .../java/testSuite/ErrorArithmeticFP1.java | 12 ------- .../java/testSuite/ErrorArithmeticFP2.java | 15 -------- .../java/testSuite/ErrorArithmeticFP3.java | 13 ------- .../java/testSuite/ErrorArithmeticFP4.java | 14 -------- .../java/testSuite/ErrorBoxedBoolean.java | 11 ------ .../main/java/testSuite/ErrorBoxedDouble.java | 11 ------ .../java/testSuite/ErrorBoxedInteger.java | 11 ------ .../main/java/testSuite/ErrorBoxedTypes.java | 21 +++++++++++ .../testSuite/ErrorFunctionInvocation.java | 34 +++++++++++++++++- .../testSuite/ErrorFunctionInvocation1.java | 32 ----------------- .../ErrorFunctionInvocationParams.java | 19 ---------- .../java/testSuite/ErrorIfAssignment.java | 9 ++++- .../java/testSuite/ErrorIfAssignment2.java | 11 ------ .../ErrorInstanceVarInRefinement.java | 12 ++++++- .../ErrorInstanceVarInRefinementIf.java | 16 --------- ...rorLongUsage2.java => ErrorLongUsage.java} | 15 ++++++-- .../main/java/testSuite/ErrorLongUsage1.java | 16 --------- .../testSuite/ErrorLongUsagePredicates.java | 19 ++++++++++ .../testSuite/ErrorLongUsagePredicates1.java | 10 ------ .../testSuite/ErrorLongUsagePredicates2.java | 10 ------ .../testSuite/ErrorLongUsagePredicates3.java | 10 ------ ...rorRecursion1.java => ErrorRecursion.java} | 8 +++-- ...ay2.java => ErrorSearchValueIntArray.java} | 9 +++-- .../testSuite/ErrorSearchValueIntArray1.java | 21 ----------- .../java/testSuite/ErrorSpecificValuesIf.java | 10 ++++++ .../testSuite/ErrorSpecificValuesIf2.java | 16 --------- .../errorMax/{MathAbs.java => MathMax.java} | 4 +-- 30 files changed, 178 insertions(+), 280 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java rename liquidjava-example/src/main/java/testSuite/{ErrorLongUsage2.java => ErrorLongUsage.java} (58%) delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java rename liquidjava-example/src/main/java/testSuite/{ErrorRecursion1.java => ErrorRecursion.java} (53%) rename liquidjava-example/src/main/java/testSuite/{ErrorSearchValueIntArray2.java => ErrorSearchValueIntArray.java} (72%) delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java rename liquidjava-example/src/main/java/testSuite/math/errorMax/{MathAbs.java => MathMax.java} (75%) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java index 592df70da..f4cca99c0 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java @@ -4,16 +4,28 @@ @SuppressWarnings("unused") public class ErrorAfterIf { - public void have2(int a, int b) { + public void afterIf1(int a, int b) { @Refinement("pos > 0") int pos = 10; if (a > 0 && b > 0) { pos = a; } else { - if (b > 0) pos = b; + if (b > 0) + pos = b; } @Refinement("_ == a || _ == b") int r = pos; // Refinement Error } + + public void afterIf2() { + @Refinement("k > 0 && k < 100") + int k = 5; + if (k > 7) { + k = 9; + } + k = 50; + @Refinement("_ < 10") + int m = k; // Refinement Error + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java deleted file mode 100644 index 3082a9899..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java +++ /dev/null @@ -1,17 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorAfterIf2 { - public static void main(String[] args) { - @Refinement("k > 0 && k < 100") - int k = 5; - if (k > 7) { - k = 9; - } - k = 50; - @Refinement("_ < 10") - int m = k; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java new file mode 100644 index 000000000..05ee1e598 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java @@ -0,0 +1,36 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorArithmeticFP { + + private static void arithmetic1(){ + @Refinement("_ > 5.0") + double a = 5.0; // Refinement Error + } + + private static void arithmetic2(){ + @Refinement("_ > 5.0") + double a = 5.5; + + @Refinement("_ == 10.0") + double c = a * 2.0; // Refinement Error + } + + private static void arithmetic3(){ + @Refinement("_ > 5.0") + double a = 5.5; + + @Refinement("_ < -5.5") + double d = -a; // Refinement Error + } + + private static void arithmetic4(){ + @Refinement("_ > 5.0") + double a = 5.5; + + @Refinement("_ < -5.5") + double d = -(a - 2.0); // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java deleted file mode 100644 index 83359da0f..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java +++ /dev/null @@ -1,12 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorArithmeticFP1 { - - public static void main(String[] args) { - @Refinement("_ > 5.0") - double a = 5.0; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java deleted file mode 100644 index a3816b2e3..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java +++ /dev/null @@ -1,15 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorArithmeticFP2 { - - public static void main(String[] args) { - @Refinement("_ > 5.0") - double a = 5.5; - - @Refinement("_ == 10.0") - double c = a * 2.0; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java deleted file mode 100644 index ffeaf1a17..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java +++ /dev/null @@ -1,13 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorArithmeticFP3 { - public static void main(String[] args) { - @Refinement("_ > 5.0") - double a = 5.5; - @Refinement("_ < -5.5") - double d = -a; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java deleted file mode 100644 index f7a105064..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java +++ /dev/null @@ -1,14 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorArithmeticFP4 { - public static void main(String[] args) { - @Refinement("_ > 5.0") - double a = 5.5; - - @Refinement("_ < -5.5") - double d = -(a - 2.0); // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java deleted file mode 100644 index acfaf4beb..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java +++ /dev/null @@ -1,11 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorBoxedBoolean { - public static void main(String[] args) { - @Refinement("_ == true") - Boolean b = false; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java deleted file mode 100644 index d51e1916f..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java +++ /dev/null @@ -1,11 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorBoxedDouble { - public static void main(String[] args) { - @Refinement("_ > 0") - Double d = -1.0; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java deleted file mode 100644 index 883569cde..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java +++ /dev/null @@ -1,11 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorBoxedInteger { - public static void main(String[] args) { - @Refinement("_ > 0") - Integer j = -1; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java new file mode 100644 index 000000000..095c2db6f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorBoxedTypes { + public static void boxedBoolean() { + @Refinement("_ == true") + Boolean b = false; // Refinement Error + } + + public static void boxedInteger() { + @Refinement("_ > 0") + Integer j = -1; // Refinement Error + } + + public static void boxedDouble() { + @Refinement("_ > 0") + Double d = -1.0; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java index d7a03f16b..e2f51f433 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java @@ -11,9 +11,41 @@ public static int posMult(@Refinement("a == 10") int a, @Refinement("_ < a && _ return y - 10; } - public static void main(String[] args) { + @Refinement("_ == 2") + private static int getTwo() { + return 1 + 1; + } + + @Refinement(" _ == 0") + private static int getZero() { + return 0; + } + + @Refinement("_ == 1") + private static int getOne() { + @Refinement("_ == 0") + int a = getZero(); + return a + 1; + } + + public static void invocation1() { @Refinement("_ > 10") int p = 10; // Refinement Error p = posMult(10, 4); } + + public static void invocation2() { + @Refinement("_ < 1") + int b = getZero(); + + @Refinement("_ > 0") + int c = getOne(); + c = getZero(); // Refinement Error + } + + public static void invocationWParams() { + @Refinement("_ >= 0") + int p = 10; + p = posMult(10, 12); // Refinement Error + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java deleted file mode 100644 index c83e4d2d0..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java +++ /dev/null @@ -1,32 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorFunctionInvocation1 { - @Refinement("_ == 2") - private static int getTwo() { - return 1 + 1; - } - - @Refinement(" _ == 0") - private static int getZero() { - return 0; - } - - @Refinement("_ == 1") - private static int getOne() { - @Refinement("_ == 0") - int a = getZero(); - return a + 1; - } - - public static void main(String[] args) { - @Refinement("_ < 1") - int b = getZero(); - - @Refinement("_ > 0") - int c = getOne(); - c = getZero(); // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java deleted file mode 100644 index 852a80150..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java +++ /dev/null @@ -1,19 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorFunctionInvocationParams { - @Refinement("_ >= a") - public static int posMult(@Refinement("a == 10") int a, @Refinement("_ < a && _ > 0") int b) { - @Refinement("y > 30") - int y = 50; - return y - 10; - } - - public static void main(String[] args) { - @Refinement("_ >= 0") - int p = 10; - p = posMult(10, 12); // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java index 426b7c3f7..ecaa52a27 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java @@ -4,7 +4,7 @@ @SuppressWarnings("unused") public class ErrorIfAssignment { - public static void main(String[] args) { + public static void ifAssignment1() { @Refinement("_ < 10") int a = 5; @@ -15,4 +15,11 @@ public static void main(String[] args) { a = 10; // Refinement Error } } + + public static void ifAssignment2() { + @Refinement("_ < 10") + int a = 5; + if (a < 0) + a = 100; // Refinement Error + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java deleted file mode 100644 index ce67a6dc2..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java +++ /dev/null @@ -1,11 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorIfAssignment2 { - public static void main(String[] args) { - @Refinement("_ < 10") - int a = 5; - if (a < 0) a = 100; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java index b62a0dd22..7a686198c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java @@ -4,7 +4,17 @@ @SuppressWarnings("unused") public class ErrorInstanceVarInRefinement { - public static void main(String[] args) { + public static void varInRefinement1() { + @Refinement("_ < 10") + int a = 6; + if (a > 0) { + a = -2; + @Refinement("b < a") + int b = -3; // Refinement Error + } + } + + public static void varInRefinement2() { @Refinement("_ < 10") int a = 6; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java deleted file mode 100644 index 43b41e88c..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java +++ /dev/null @@ -1,16 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorInstanceVarInRefinementIf { - public static void main(String[] args) { - @Refinement("_ < 10") - int a = 6; - if (a > 0) { - a = -2; - @Refinement("b < a") - int b = -3; // Refinement Error - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java similarity index 58% rename from liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java rename to liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java index 127434c31..524a9a02a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java @@ -3,14 +3,23 @@ import liquidjava.specification.Refinement; @SuppressWarnings("unused") -public class ErrorLongUsage2 { - +public class ErrorLongUsage { @Refinement(" _ > 40") public static long doubleBiggerThanTwenty(@Refinement("a > 20") long a) { return a * 2; } - public static void main(String[] args) { + public static void longUsage1() { + @Refinement("a > 5") + long a = 9L; + + if (a > 5) { + @Refinement("b < 50") + long b = a * 10; // Refinement Error + } + } + + public static void longUsage2() { @Refinement("a > 5") long a = 9L; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java deleted file mode 100644 index aa9b6d8e6..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java +++ /dev/null @@ -1,16 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorLongUsage1 { - public static void main(String[] args) { - @Refinement("a > 5") - long a = 9L; - - if (a > 5) { - @Refinement("b < 50") - long b = a * 10; // Refinement Error - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java new file mode 100644 index 000000000..8e2cea409 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java @@ -0,0 +1,19 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorLongUsagePredicates { + void testLargeSubtractionWrong() { + @Refinement("v - 9007199254740992 == 2") + long v = 9007199254740993L; // Refinement Error + } + void testUUID(){ + @Refinement("((v/4096) % 16) == 2") + long v = 0x01000000122341666L; // Refinement Error + } + + void testWrongSign() { + @Refinement("v < 0") + long v = 42L; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java deleted file mode 100644 index 93495c066..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java +++ /dev/null @@ -1,10 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorLongUsagePredicates1 { - void testUUID(){ - @Refinement("((v/4096) % 16) == 2") - long v = 0x01000000122341666L; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java deleted file mode 100644 index 7b6978ca4..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java +++ /dev/null @@ -1,10 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorLongUsagePredicates2 { - void testLargeSubtractionWrong() { - @Refinement("v - 9007199254740992 == 2") - long v = 9007199254740993L; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java deleted file mode 100644 index d460abe78..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java +++ /dev/null @@ -1,10 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorLongUsagePredicates3 { - void testWrongSign() { - @Refinement("v < 0") - long v = 42L; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursion.java similarity index 53% rename from liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java rename to liquidjava-example/src/main/java/testSuite/ErrorRecursion.java index 9ddc0e4ec..56b7f4f86 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursion.java @@ -2,11 +2,13 @@ import liquidjava.specification.Refinement; -public class ErrorRecursion1 { +public class ErrorRecursion { @Refinement(" _ == 0") public static int untilZero(@Refinement("k >= 0") int k) { - if (k == 1) return 0; - else return untilZero(k - 1); // Refinement Error + if (k == 1) + return 0; + else + return untilZero(k - 1); // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java similarity index 72% rename from liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java rename to liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java index 05c6360d8..01d213a9c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java @@ -3,7 +3,7 @@ import liquidjava.specification.Refinement; import liquidjava.specification.RefinementPredicate; -public class ErrorSearchValueIntArray2 { +public class ErrorSearchValueIntArray { @RefinementPredicate("ghost int length(int[])") @Refinement("(_ >= -1) && (_ < length(l))") @@ -14,8 +14,13 @@ public static int getIndexWithValue( else return getIndexWithValue(l, i + 1, val); } - public static void main(String[] args) { + public static void searchValue1() { int[] arr = new int[10]; getIndexWithValue(arr, arr.length, 1000); // Refinement Error } + + public static void searchValue2(String[] args) { + int[] arr = new int[0]; + getIndexWithValue(arr, 0, 1000); // Refinement Error + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java deleted file mode 100644 index f7e4b0b9b..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java +++ /dev/null @@ -1,21 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; -import liquidjava.specification.RefinementPredicate; - -public class ErrorSearchValueIntArray1 { - - @RefinementPredicate("ghost int length(int[])") - @Refinement("(_ >= -1) && (_ < length(l))") - public static int getIndexWithValue( - @Refinement("length(l) > 0") int[] l, @Refinement("i >= 0 && i < length(l)") int i, int val) { - if (l[i] == val) return i; - if (i >= l.length - 1) return -1; - else return getIndexWithValue(l, i + 1, val); - } - - public static void main(String[] args) { - int[] arr = new int[0]; - getIndexWithValue(arr, 0, 1000); // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java index d44efc462..dd096788e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java @@ -19,4 +19,14 @@ public static void addZ(@Refinement("a > 0") int a) { int b = d; // Refinement Error } } + + public static void addZ2() { + @Refinement("_ > 10") + int a = 15; + if (a > 14) { + a = 12; + @Refinement("_ < 11") + int c = a; // Refinement Error + } + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java deleted file mode 100644 index 1ec4ec329..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java +++ /dev/null @@ -1,16 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorSpecificValuesIf2 { - public static void main(String[] args) { - @Refinement("_ > 10") - int a = 15; - if (a > 14) { - a = 12; - @Refinement("_ < 11") - int c = a; // Refinement Error - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMax/MathAbs.java b/liquidjava-example/src/main/java/testSuite/math/errorMax/MathMax.java similarity index 75% rename from liquidjava-example/src/main/java/testSuite/math/errorMax/MathAbs.java rename to liquidjava-example/src/main/java/testSuite/math/errorMax/MathMax.java index 783fc469a..49f6d092d 100644 --- a/liquidjava-example/src/main/java/testSuite/math/errorMax/MathAbs.java +++ b/liquidjava-example/src/main/java/testSuite/math/errorMax/MathMax.java @@ -3,12 +3,12 @@ import liquidjava.specification.Refinement; @SuppressWarnings("unused") -public class MathAbs { +public class MathMax { public static void main(String[] args) { @Refinement("true") int ab = Math.abs(-9); @Refinement("_ == 9") - int ab1 = -ab; // Refinement Error + int ab1 = Math.max(-9, -ab); // Refinement Error } } From 834ff5e666d28190b4c352b6be5b5e2745eb32c7 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Tue, 17 Mar 2026 14:33:35 +0000 Subject: [PATCH 09/12] Merged invalid refinements and unary operators testMultiple should be refactored in another PR, as warning support isn't implemented. --- .../main/java/testSuite/ErrorInvalidRefinement.java | 9 ++++++++- .../testSuite/ErrorInvalidRefinementParameter.java | 12 ------------ .../java/testSuite/ErrorInvalidRefinementReturn.java | 10 ---------- .../src/main/java/testSuite/ErrorUnaryOpMinus.java | 11 ----------- .../src/main/java/testSuite/ErrorUnaryOperators.java | 8 +++++++- 5 files changed, 15 insertions(+), 35 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java index ff54ad612..612bd2720 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java @@ -5,8 +5,15 @@ @SuppressWarnings("unused") public class ErrorInvalidRefinement { - void test() { + void invalidRefinement1() { @Refinement("x") // Invalid Refinement Error int x = 0; } + + void invalidRefinement2(@Refinement("y + 1") int y) { // Invalid Refinement Error + } + + @Refinement("_ * 2") // Invalid Refinement Error + void invalidRefinement3() { + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java deleted file mode 100644 index c7349fac0..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java +++ /dev/null @@ -1,12 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorInvalidRefinementParameter { - - void testInvalidRefinement(@Refinement("y + 1") int y) {} // Invalid Refinement Error - - int otherMethod() { - return -1; - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java deleted file mode 100644 index f4af39510..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java +++ /dev/null @@ -1,10 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorInvalidRefinementReturn { - - @Refinement("_ * 2") // Invalid Refinement Error - void test() { - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java deleted file mode 100644 index a4db398d9..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java +++ /dev/null @@ -1,11 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorUnaryOpMinus { - public static void main(String[] args) { - @Refinement("b > 0") - int b = 8; - b = -b; // Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java index f40a0e98e..df4c61112 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java @@ -4,7 +4,7 @@ @SuppressWarnings("unused") public class ErrorUnaryOperators { - public static void main(String[] args) { + public static void unaryOperator1() { @Refinement("_ < 10") int v = 3; v--; @@ -12,4 +12,10 @@ public static void main(String[] args) { int s = 10; s--; // Refinement Error } + + public static void unaryOperator2() { + @Refinement("b > 0") + int b = 8; + b = -b; // Refinement Error + } } From 0ac568eda9765d3e09837e0310648bc4bdb8335b Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Tue, 17 Mar 2026 15:31:47 +0000 Subject: [PATCH 10/12] Fixed naming for some tests Eventually, function modifiers should be uniformed, as well as some other names. --- .../main/java/testSuite/ErrorArithmeticFP.java | 8 ++++---- .../main/java/testSuite/ErrorBoxedTypes.java | 6 +++--- .../src/main/java/testSuite/ErrorChars.java | 9 ++++----- .../testSuite/ErrorDotNotationMultiple.java | 7 ++++--- .../main/java/testSuite/ErrorGhostNotFound.java | 2 +- .../testSuite/ErrorInstanceVarInRefinement.java | 4 ++-- .../java/testSuite/ErrorInvalidRefinement.java | 6 +++--- .../testSuite/ErrorLongUsagePredicates.java | 17 +++++++++-------- .../java/testSuite/ErrorTrafficLightRGB.java | 4 ++-- .../java/testSuite/ErrorUnaryOperators.java | 4 ++-- 10 files changed, 34 insertions(+), 33 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java index 05ee1e598..1ee5fc28e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java @@ -5,12 +5,12 @@ @SuppressWarnings("unused") public class ErrorArithmeticFP { - private static void arithmetic1(){ + private static void arithmetic1() { @Refinement("_ > 5.0") double a = 5.0; // Refinement Error } - private static void arithmetic2(){ + private static void arithmetic2() { @Refinement("_ > 5.0") double a = 5.5; @@ -18,7 +18,7 @@ private static void arithmetic2(){ double c = a * 2.0; // Refinement Error } - private static void arithmetic3(){ + private static void arithmetic3() { @Refinement("_ > 5.0") double a = 5.5; @@ -26,7 +26,7 @@ private static void arithmetic3(){ double d = -a; // Refinement Error } - private static void arithmetic4(){ + private static void arithmetic4() { @Refinement("_ > 5.0") double a = 5.5; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java index 095c2db6f..ddf42dcb9 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedTypes.java @@ -4,17 +4,17 @@ @SuppressWarnings("unused") public class ErrorBoxedTypes { - public static void boxedBoolean() { + public static void errorBoxedBoolean() { @Refinement("_ == true") Boolean b = false; // Refinement Error } - public static void boxedInteger() { + public static void errorBoxedInteger() { @Refinement("_ > 0") Integer j = -1; // Refinement Error } - public static void boxedDouble() { + public static void errorBoxedDouble() { @Refinement("_ > 0") Double d = -1.0; // Refinement Error } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorChars.java b/liquidjava-example/src/main/java/testSuite/ErrorChars.java index 3fb517106..09ba67d49 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorChars.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorChars.java @@ -3,12 +3,11 @@ import liquidjava.specification.Refinement; public class ErrorChars { - - void test() { - printLetter('$'); // Refinement Error - } - void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) { System.out.println(c); } + + public static void main(String[] args) { + printLetter('$'); // Refinement Error + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java index 0fe943667..6404d9aef 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java @@ -7,10 +7,11 @@ @Ghost("int size") public class ErrorDotNotationMultiple { - @StateRefinement(to="size() == 0") - public ErrorDotNotationMultiple() {} + @StateRefinement(to = "size() == 0") + public ErrorDotNotationMultiple() { + } - void test() { + public static void main(String[] args) { @Refinement("_ == this.not.size()") // Syntax Error int x = 0; } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java index c56607b25..c9ea3e159 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java @@ -4,7 +4,7 @@ public class ErrorGhostNotFound { - public void test() { + public static void main(String[] args) { @Refinement("notFound(x)") int x = 5; // Not Found Error } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java index 7a686198c..fdaa92a9c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java @@ -4,7 +4,7 @@ @SuppressWarnings("unused") public class ErrorInstanceVarInRefinement { - public static void varInRefinement1() { + public static void varInRefinementInIf() { @Refinement("_ < 10") int a = 6; if (a > 0) { @@ -14,7 +14,7 @@ public static void varInRefinement1() { } } - public static void varInRefinement2() { + public static void varInRefinement() { @Refinement("_ < 10") int a = 6; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java index 612bd2720..0f2853ac9 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java @@ -5,15 +5,15 @@ @SuppressWarnings("unused") public class ErrorInvalidRefinement { - void invalidRefinement1() { + void invalidRefinement() { @Refinement("x") // Invalid Refinement Error int x = 0; } - void invalidRefinement2(@Refinement("y + 1") int y) { // Invalid Refinement Error + void invalidRefinementParameter(@Refinement("y + 1") int y) { // Invalid Refinement Error } @Refinement("_ * 2") // Invalid Refinement Error - void invalidRefinement3() { + void invalidRefinementReturn() { } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java index 8e2cea409..fef6a5899 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java @@ -3,17 +3,18 @@ import liquidjava.specification.Refinement; public class ErrorLongUsagePredicates { - void testLargeSubtractionWrong() { - @Refinement("v - 9007199254740992 == 2") + void errorLargeSubtraction() { + @Refinement("v - 9007199254740992 == 2") long v = 9007199254740993L; // Refinement Error - } - void testUUID(){ + } + + void errorUUID() { @Refinement("((v/4096) % 16) == 2") long v = 0x01000000122341666L; // Refinement Error } - - void testWrongSign() { - @Refinement("v < 0") - long v = 42L; // Refinement Error + + void errorWrongSign() { + @Refinement("v < 0") + long v = 42L; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java index 3f5d8eb9b..e1b38235d 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java @@ -4,7 +4,7 @@ import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; -@StateSet({"green", "amber", "red"}) +@StateSet({ "green", "amber", "red" }) public class ErrorTrafficLightRGB { @Refinement("r >= 0 && r <= 255") @@ -44,7 +44,7 @@ public void transitionToRed() { b = 1; } - public static void name() { + public static void main(String[] args) { ErrorTrafficLightRGB tl = new ErrorTrafficLightRGB(); tl.transitionToAmber(); tl.transitionToRed(); diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java index df4c61112..de8571568 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java @@ -4,7 +4,7 @@ @SuppressWarnings("unused") public class ErrorUnaryOperators { - public static void unaryOperator1() { + public static void errorUnaryOperators() { @Refinement("_ < 10") int v = 3; v--; @@ -13,7 +13,7 @@ public static void unaryOperator1() { s--; // Refinement Error } - public static void unaryOperator2() { + public static void errorUnaryOperatorMinus() { @Refinement("b > 0") int b = 8; b = -b; // Refinement Error From 136f8db807c5cb779e5faa9f78b265791cc19a96 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Tue, 17 Mar 2026 15:39:37 +0000 Subject: [PATCH 11/12] Fixed static keyword --- liquidjava-example/src/main/java/testSuite/ErrorChars.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorChars.java b/liquidjava-example/src/main/java/testSuite/ErrorChars.java index 09ba67d49..dc4a04dde 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorChars.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorChars.java @@ -3,7 +3,7 @@ import liquidjava.specification.Refinement; public class ErrorChars { - void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) { + static void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) { System.out.println(c); } From edb012b2d05e0048810fe6689e304cc66a72eb23 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Mon, 30 Mar 2026 01:11:53 +0100 Subject: [PATCH 12/12] Fixed failures due to changes from #185 --- .../src/main/java/testSuite/ErrorAliasArgumentSize.java | 4 ++-- .../src/main/java/testSuite/ErrorAliasNotFound.java | 4 ++-- .../src/main/java/testSuite/ErrorAliasTypeMismatch.java | 4 ++-- .../src/main/java/testSuite/ErrorAssignmentBeforeReturn.java | 3 +-- .../src/main/java/testSuite/ErrorGhostNotFound.java | 4 ++-- .../src/main/java/testSuite/ErrorTypeInRefinements.java | 4 ++-- .../state_multiple_error/InputStreamReaderRefinements.java | 4 ++-- 7 files changed, 13 insertions(+), 14 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java index c01f2c215..030d3d448 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)") - int j = 15; // Argument Mismatch Error + @Refinement("InRange(j, 10)") // 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 116c68f33..e9da55860 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)") - int x = 5; // Not Found Error + @Refinement("UndefinedAlias(x)") // Not Found Error + int x = 5; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java index 0343401bd..0618ae83a 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(_)") - double positive = positiveGrade2; // Argument Mismatch Error + @Refinement("Positive(_)") // Argument Mismatch Error + double positive = positiveGrade2; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java b/liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java index 8b5eff5a0..de75f2c72 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java @@ -1,4 +1,3 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @@ -7,6 +6,6 @@ public class ErrorAssignmentBeforeReturn { @Refinement("_ > 0") static int example(int x) { x = x + 1; - return x; + return x; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java index c9ea3e159..49fd90ad0 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)") - int x = 5; // Not Found Error + @Refinement("notFound(x)") // Not Found Error + int x = 5; } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java index d2c5c8d3f..965a238f8 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)") - boolean b = true; // Error + @Refinement("(b == 6)") // Error + boolean b = true; } } 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 85c57be4a..3ca9bb8a4 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,8 +12,8 @@ @StateSet({"alreadyRead", "nothingRead"}) public interface InputStreamReaderRefinements { - @StateRefinement(to = "open(this) && close(this)") - public void InputStreamReader(InputStream in); // State Conflict Error + @StateRefinement(to = "open(this) && close(this)") // State Conflict Error + public void InputStreamReader(InputStream in); @StateRefinement(from = "open(this)", to = "open(this) && alreadyRead(this)") @Refinement("(_ >= -1) && (_ <= 127)")