Merge branch 'CatarinaGamboa:main' into main

Author: fc53679

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

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

@@ -0,0 +1,6 @@
+package testSuite;
+
+import liquidjava.specification.RefinementAlias;
+
+@RefinementAlias("Positive(v) { v > 0 }")
+public class ErrorMissingAliasTypeParameter {}

liquidjava-example/src/main/java/testSuite/classes/arraylist_correct/ArrayListRefinements.java

@@ -12,7 +12,7 @@ public interface ArrayListRefinements<E> {
     public void ArrayList();
 
     @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
-    public void add(E e);
+    public boolean add(E e);
 
     //	@Refinement("size(_) == size(this)")
     //	public Object clone();

liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java

@@ -11,7 +11,7 @@ public interface StackRefinements<E> {
 	public void Stack();
 
 	@StateRefinement(to="size(this) == size(old(this)) + 1")
-	public boolean push(E elem);
+	public E push(E elem);
 
 	@StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1")
 	public E pop();

liquidjava-example/src/main/java/testSuite/classes/method_overload_error/DummySemaphoreRefinements.java

@@ -0,0 +1,12 @@
+package testSuite.classes.method_overload_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+
+@ExternalRefinementsFor("java.util.concurrent.Semaphore")
+public interface DummySemaphoreRefinements {
+
+	public abstract void acquire();
+
+	public abstract void acquire(@Refinement("_ >= 0") int permits) throws InterruptedException;
+}

liquidjava-example/src/main/java/testSuite/classes/method_overload_error/TestMethodOverloadEror.java

@@ -0,0 +1,10 @@
+package testSuite.classes.method_overload_error;
+
+import java.util.concurrent.Semaphore;
+
+public class TestMethodOverloadEror {
+	public static void main(String[] args) throws InterruptedException {
+		Semaphore sem = new Semaphore(1);
+		sem.acquire(-1);
+	}
+}

liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java

@@ -16,13 +16,13 @@ public interface MathRefinements {
     public int abs(int arg0);
 
     @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)")
-    public int abs(long arg0);
+    public long abs(long arg0);
 
     @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)")
-    public int abs(float arg0);
+    public float abs(float arg0);
 
     @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)")
-    public int abs(double arg0);
+    public double abs(double arg0);
 
     @Refinement(" _ == a+b")
     public int addExact(int a, int b);
@@ -43,13 +43,13 @@ public interface MathRefinements {
     public int decrementExact(int a);
 
     @Refinement("_ == (a-1)")
-    public int decrementExact(long a);
+    public long decrementExact(long a);
 
     @Refinement("_ == (a+1)")
     public int incrementExact(int a);
 
     @Refinement("_ == (a+1)")
-    public int incrementExact(long a);
+    public long incrementExact(long a);
 
     @Refinement("(a > b)? (_ == a):(_ == b)")
     public int max(int a, int b);