Improve test suite

liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java

@@ -1,4 +1,3 @@
-// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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
     }
 }

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
     }
 }

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
     }
 }

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;
     }
 }

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
     }
 }

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
     }
 }

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
     }
 }

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
     }
 }

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
+    }
+}

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
     }
 }

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
     }
 }

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
     }
 }

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
+    }
+}

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
     }
 }

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
     }
 }

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
     }
 }