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..f4cca99c0 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java @@ -1,20 +1,31 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @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; + 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 3ae6ed8e3..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java +++ /dev/null @@ -1,18 +0,0 @@ -// Refinement Error -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; - } -} 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/ErrorArithmeticFP.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP.java new file mode 100644 index 000000000..1ee5fc28e --- /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 45239bc66..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java +++ /dev/null @@ -1,13 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorArithmeticFP1 { - - public static void main(String[] args) { - @Refinement("_ > 5.0") - double a = 5.0; - } -} 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 16e58df78..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java +++ /dev/null @@ -1,16 +0,0 @@ -// Refinement Error -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; - } -} 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 ae85bc500..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java +++ /dev/null @@ -1,14 +0,0 @@ -// Refinement Error -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; - } -} 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 88eed94ca..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java +++ /dev/null @@ -1,15 +0,0 @@ -// Refinement Error -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); - } -} 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 deleted file mode 100644 index 93c6a3c12..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java +++ /dev/null @@ -1,12 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorBoxedBoolean { - public static void main(String[] args) { - @Refinement("_ == true") - Boolean b = false; - } -} 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 643b509ab..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java +++ /dev/null @@ -1,12 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorBoxedDouble { - public static void main(String[] args) { - @Refinement("_ > 0") - Double d = -1.0; - } -} 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 2d937e208..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java +++ /dev/null @@ -1,12 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorBoxedInteger { - public static void main(String[] args) { - @Refinement("_ > 0") - Integer j = -1; - } -} 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..ddf42dcb9 --- /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 errorBoxedBoolean() { + @Refinement("_ == true") + Boolean b = false; // Refinement Error + } + + public static void errorBoxedInteger() { + @Refinement("_ > 0") + Integer j = -1; // Refinement Error + } + + 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 cbaf4b1d9..dc4a04dde 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorChars.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorChars.java @@ -1,15 +1,13 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; public class ErrorChars { - - void test() { - printLetter('$'); // error + static void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) { + System.out.println(c); } - 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/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..6404d9aef 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; @@ -8,11 +7,12 @@ @Ghost("int size") public class ErrorDotNotationMultiple { - @StateRefinement(to="size() == 0") - public ErrorDotNotationMultiple() {} + @StateRefinement(to = "size() == 0") + public ErrorDotNotationMultiple() { + } - void test() { - @Refinement("_ == this.not.size()") + public static void main(String[] args) { + @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..e2f51f433 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; @@ -12,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; + 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 e4309a4c0..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java +++ /dev/null @@ -1,33 +0,0 @@ -// Refinement Error -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(); - } -} 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 6d1fa4736..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java +++ /dev/null @@ -1,20 +0,0 @@ -// Refinement Error -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); - } -} 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..c9ea3e159 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java @@ -1,12 +1,11 @@ -// Not Found Error package testSuite; import liquidjava.specification.Refinement; public class ErrorGhostNotFound { - public void test() { + public static void main(String[] args) { @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..ecaa52a27 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java @@ -1,11 +1,10 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @SuppressWarnings("unused") public class ErrorIfAssignment { - public static void main(String[] args) { + public static void ifAssignment1() { @Refinement("_ < 10") int a = 5; @@ -13,7 +12,14 @@ public static void main(String[] args) { @Refinement("b > 0") int b = a; b++; - a = 10; + 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 19692a5a9..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java +++ /dev/null @@ -1,12 +0,0 @@ -// Refinement Error -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; - } -} 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..fdaa92a9c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java @@ -1,15 +1,24 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @SuppressWarnings("unused") public class ErrorInstanceVarInRefinement { - public static void main(String[] args) { + public static void varInRefinementInIf() { + @Refinement("_ < 10") + int a = 6; + if (a > 0) { + a = -2; + @Refinement("b < a") + int b = -3; // Refinement Error + } + } + + public static void varInRefinement() { @Refinement("_ < 10") 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 deleted file mode 100644 index f0a973fd9..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java +++ /dev/null @@ -1,17 +0,0 @@ -// Refinement Error -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; - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java index 6933955fe..0f2853ac9 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; @@ -6,8 +5,15 @@ @SuppressWarnings("unused") public class ErrorInvalidRefinement { - void test() { - @Refinement("x") + void invalidRefinement() { + @Refinement("x") // Invalid Refinement Error int x = 0; } + + void invalidRefinementParameter(@Refinement("y + 1") int y) { // Invalid Refinement Error + } + + @Refinement("_ * 2") // Invalid Refinement Error + void invalidRefinementReturn() { + } } 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 c6a92e459..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java +++ /dev/null @@ -1,13 +0,0 @@ -// Invalid Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorInvalidRefinementParameter { - - void testInvalidRefinement(@Refinement("y + 1") int y) {} - - 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 b106518b4..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java +++ /dev/null @@ -1,11 +0,0 @@ -// Invalid Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorInvalidRefinementReturn { - - @Refinement("_ * 2") - 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/ErrorLongUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java new file mode 100644 index 000000000..524a9a02a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorLongUsage { + @Refinement(" _ > 40") + public static long doubleBiggerThanTwenty(@Refinement("a > 20") long a) { + return a * 2; + } + + 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; + + @Refinement("c > 40") + long c = doubleBiggerThanTwenty(a * 2); // Refinement Error + } +} 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 2bc1d1f62..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java +++ /dev/null @@ -1,17 +0,0 @@ -// Refinement Error -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; - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java deleted file mode 100644 index fe5a231ab..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java +++ /dev/null @@ -1,21 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -@SuppressWarnings("unused") -public class ErrorLongUsage2 { - - @Refinement(" _ > 40") - public static long doubleBiggerThanTwenty(@Refinement("a > 20") long a) { - return a * 2; - } - - public static void main(String[] args) { - @Refinement("a > 5") - long a = 9L; - - @Refinement("c > 40") - long c = doubleBiggerThanTwenty(a * 2); - } -} 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..fef6a5899 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates.java @@ -0,0 +1,20 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorLongUsagePredicates { + void errorLargeSubtraction() { + @Refinement("v - 9007199254740992 == 2") + long v = 9007199254740993L; // Refinement Error + } + + void errorUUID() { + @Refinement("((v/4096) % 16) == 2") + long v = 0x01000000122341666L; // Refinement Error + } + + void errorWrongSign() { + @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 55504b0d2..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java +++ /dev/null @@ -1,11 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorLongUsagePredicates1 { - void testUUID(){ - @Refinement("((v/4096) % 16) == 2") - long v = 0x01000000122341666L; - } -} \ 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 deleted file mode 100644 index fc760314f..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java +++ /dev/null @@ -1,11 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorLongUsagePredicates2 { - void testLargeSubtractionWrong() { - @Refinement("v - 9007199254740992 == 2") - long v = 9007199254740993L; - } -} \ 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 deleted file mode 100644 index e5412994a..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java +++ /dev/null @@ -1,11 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorLongUsagePredicates3 { - void testWrongSign() { - @Refinement("v < 0") - long v = 42L; - } -} \ 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/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 518d351ee..56b7f4f86 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursion.java @@ -1,13 +1,14 @@ -// Refinement Error package testSuite; 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); + if (k == 1) + return 0; + 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/ErrorSearchValueIntArray2.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java similarity index 64% rename from liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java rename to liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java index 944b7e6f5..01d213a9c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java @@ -1,10 +1,9 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; import liquidjava.specification.RefinementPredicate; -public class ErrorSearchValueIntArray2 { +public class ErrorSearchValueIntArray { @RefinementPredicate("ghost int length(int[])") @Refinement("(_ >= -1) && (_ < length(l))") @@ -15,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); + 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 f7a968904..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java +++ /dev/null @@ -1,22 +0,0 @@ -// Refinement Error -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); - } -} 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..dd096788e 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,17 @@ 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 + } + } + + 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 2cae544c5..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java +++ /dev/null @@ -1,17 +0,0 @@ -// Refinement Error -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; - } - } -} 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..e1b38235d 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java @@ -1,11 +1,10 @@ -// State Refinement Error package testSuite; import liquidjava.specification.Refinement; import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; -@StateSet({"green", "amber", "red"}) +@StateSet({ "green", "amber", "red" }) public class ErrorTrafficLightRGB { @Refinement("r >= 0 && r <= 255") @@ -45,10 +44,10 @@ public void transitionToRed() { b = 1; } - public static void name() { + public static void main(String[] args) { 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 deleted file mode 100644 index 73eb1529a..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java +++ /dev/null @@ -1,12 +0,0 @@ -// Refinement Error -package testSuite; - -import liquidjava.specification.Refinement; - -public class ErrorUnaryOpMinus { - public static void main(String[] args) { - @Refinement("b > 0") - int b = 8; - b = -b; - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java index b8660ea83..de8571568 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java @@ -1,16 +1,21 @@ -// Refinement Error package testSuite; import liquidjava.specification.Refinement; @SuppressWarnings("unused") public class ErrorUnaryOperators { - public static void main(String[] args) { + public static void errorUnaryOperators() { @Refinement("_ < 10") int v = 3; v--; @Refinement("_ >= 10") int s = 10; - s--; + s--; // Refinement Error + } + + public static void errorUnaryOperatorMinus() { + @Refinement("b > 0") + int b = 8; + b = -b; // 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/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-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-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/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 75c12d9ea..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; + int ab1 = Math.max(-9, -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/pom.xml b/liquidjava-verifier/pom.xml index 34ea18db5..d35a338d1 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..7c07d3c9c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -1,18 +1,22 @@ package liquidjava.api.tests; import static liquidjava.utils.TestUtils.*; + import static org.junit.Assert.fail; import java.io.IOException; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; -import java.util.Optional; +import java.util.List; import java.util.stream.Stream; + import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; +import liquidjava.utils.Pair; + import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; @@ -35,43 +39,47 @@ 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) + // 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"); + 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"); + List> expectedErrors = isDirectory ? getExpectedErrorsFromDirectory(path) + : getExpectedErrorsFromFile(path); + if (diagnostics.getErrors().size() != expectedErrors.size()) { + System.out.println("Multiple errors found in: " + pathName + " --- expected exactly " + + expectedErrors.size() + " errors. \n" + diagnostics.getErrorOutput()); fail(); } - LJError error = diagnostics.getErrors().iterator().next(); - if (error.getPosition() == null) { - System.out.println("Error in: " + pathName + " --- error has no position information"); - fail(); - } - if (expected.isPresent()) { - String expectedError = expected.get(); - String foundError = error.getTitle(); - if (!foundError.equalsIgnoreCase(expectedError)) { - System.out.println("Error in: " + pathName + " --- expected error: " + expectedError - + ", but found: " + foundError); - fail(); + if (!expectedErrors.isEmpty()) { + for (LJError e : diagnostics.getErrors()) { + String foundError = e.getTitle(); + int errorPosition = e.getPosition().getLine(); + boolean match = expectedErrors.stream().anyMatch( + expected -> expected.first().equals(foundError) && expected.second() == errorPosition); + + if (!match) { + System.out.println("Error in: " + pathName + " --- expected errors: " + expectedErrors + + ", but found: " + foundError + " at " + errorPosition + ". \n" + + diagnostics.getErrorOutput()); + fail(); + } } } else { - System.out.println("No expected error 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 specify each expected error in the test file as a comment on the line where the error should be reported."); fail(); } } @@ -115,7 +123,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(); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index cd15f869b..10ac4d33d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -1,13 +1,15 @@ 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; +import java.util.regex.Matcher; +import java.util.regex.Pattern; public class TestUtils { - /** * Determines if the given path indicates that the test should pass * @@ -27,41 +29,51 @@ 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; + int lineNumber = 0; + while ((line = reader.readLine()) != null) { + lineNumber++; + Pattern p = Pattern.compile("//\\s*(.*?\\bError\\b)", Pattern.CASE_INSENSITIVE); + Matcher m = p.matcher(line); + if (m.find()) { + expectedErrors.add(new Pair<>(m.group(1).trim(), lineNumber)); + } } - } 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; } }