Add Tests

Author: rcosta358

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

@@ -12,5 +12,5 @@ public interface ErrorExtRefNonExistentMethod<E> {
     public void ArrayList();
 
     @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
-    public void adddd(E e);
+    public boolean adddd(E e);
 }

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface ErrorExtRefWrongConstructor<E> {
+
+    @RefinementPredicate("int size(ArrayList l)")
+    @StateRefinement(to = "size(this) == 0")
+    public void ArrayList(String wrongParameter);
+
+    @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+    public boolean add(E e);
+}

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface ErrorExtRefWrongParameterType<E> {
+
+    @RefinementPredicate("int size(ArrayList l)")
+    @StateRefinement(to = "size(this) == 0")
+    public void ArrayList();
+
+    @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+    public boolean add(int wrongParameter);
+}

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface ErrorExtRefWrongRetType<E> {
+
+    @RefinementPredicate("int size(ArrayList l)")
+    @StateRefinement(to = "size(this) == 0")
+    public void ArrayList();
+
+    @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+    public int add(E e); // wrong return type
+}