Check Expected Errors in Tests (#126)

rcosta358 · web-flow · commit f59d1c45cd52 · 2025-12-04T11:22:00.000Z
diff --git a/README.md b/README.md
@@ -78,8 +78,6 @@ To run LiquidJava, use the Maven command below, replacing `/path/to/your/project
 ```bash
 mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project"
 ```
-*Warning: Any change to LiquidJava requires rebuilding the jar.*
-
 
 If you're on Linux/macOS, you can use the `liquidjava` script (from the repository root) to simplify the process.
 
@@ -105,10 +103,14 @@ The starter test file is `TestExamples.java`, which runs the test suite under th
 
 The test suite considers test cases:
 1. Files that start with `Correct` or `Error` (e.g., `CorrectRecursion.java`)
-2. Packages or folders that contain the word `correct` or `error` (e.g., `arraylist_correct`)
+2. Directories that contain the word `correct` or `error` (e.g., `arraylist_correct`)
 
 Therefore, the files and folders that do not follow this pattern are ignored.
 
+For failing test cases, the expected error must be specified as follows:
+1. In singular test files, the expected error (title) should be written in the first line of the file as a comment
+2. In test directories, a `.expected` file should be included in that directory with the expected error (title)
+
 ## Project Structure
 
 * **docs**: Contains documents used for the design of the language. This folder includes a [README](./docs/design/README.md) with the link to the full artifact used in the design process. It also contains initial documents used to prepare the design of the refinements language during its evaluation
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java
@@ -1,3 +1,4 @@
+// Not Found Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
@@ -8,7 +9,7 @@
 public class ErrorAliasArgumentSize {
 
     public static void main(String[] args) {
-        @Refinement("InRange( _, 10)")
+        @Refinement("InRange(j, 10)")
         int j = 15;
     }
 }
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java
@@ -1,3 +1,4 @@
+// Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java
@@ -1,3 +1,4 @@
+// Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java
@@ -1,3 +1,4 @@
+// Syntax Error
 package testSuite;
 
 import liquidjava.specification.RefinementAlias;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java b/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java
@@ -1,3 +1,4 @@
+// Syntax Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java b/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java
@@ -1,3 +1,4 @@
+// State Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java
@@ -1,3 +1,4 @@
+// Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java
@@ -1,3 +1,4 @@
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java
@@ -1,3 +1,4 @@
+// Error
 package testSuite.classes;
 
 import liquidjava.specification.Ghost;
diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected
@@ -0,0 +1 @@
+State Conflict Error
diff --git a/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java b/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java
@@ -1,3 +1,4 @@
+// State Refinement Error
 package testSuite.field_updates;
 
 import liquidjava.specification.StateRefinement;
diff --git a/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected b/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected b/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
@@ -71,16 +71,16 @@ public <R> void visitCtMethod(CtMethod<R> method) {
                 String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(),
                         prefix);
                 String[] overloads = getOverloads(targetType, method);
-                diagnostics.add(
-                        new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), prefix, overloads));
+                diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(),
+                        prefix, overloads));
             }
         } else {
             if (!methodExists(targetType, method)) {
                 String message = String.format("Could not find method '%s %s' for '%s'",
                         method.getType().getSimpleName(), method.getSignature(), prefix);
                 String[] overloads = getOverloads(targetType, method);
-                diagnostics.add(
-                        new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(), prefix, overloads));
+                diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(),
+                        prefix, overloads));
                 return;
             }
         }
diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java
diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+// Refinement Error`
`1`	`2`	`package testSuite;`
`2`	`3`
`3`	`4`	`import liquidjava.specification.Refinement;`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+// Not Found Error`
`1`	`2`	`package testSuite;`
`2`	`3`
`3`	`4`	`import liquidjava.specification.Refinement;`
`@@ -8,7 +9,7 @@`
`8`	`9`	`public class ErrorAliasArgumentSize {`
`9`	`10`
`10`	`11`	`public static void main(String[] args) {`
`11`		`- @Refinement("InRange( _, 10)")`
	`12`	`+ @Refinement("InRange(j, 10)")`
`12`	`13`	`int j = 15;`
`13`	`14`	`}`
`14`	`15`	`}`