Merge branch 'CatarinaGamboa:main' into main

Author: joaonhdelgado

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/ArrayListRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.conflicting_ghost_names_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@Ghost("int size")
+public interface ArrayListRefinements<E> {
+
+	public void ArrayList();
+	
+	@StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+	public boolean add(E elem);
+
+	public E get(@Refinement("0 <= _ && _ < size(this)") int index);
+}

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

@@ -0,0 +1,17 @@
+package testSuite.classes.conflicting_ghost_names_correct;
+
+import java.util.ArrayList;
+import java.util.Stack;
+
+public class SimpleTest {
+    public void example() {
+        ArrayList<Integer> list = new ArrayList<>();
+        list.add(10);
+        list.get(0);
+
+        Stack<Integer> stack = new Stack<>();
+		stack.push(1);
+		stack.peek();
+		stack.pop();
+    }
+}

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

@@ -0,0 +1,21 @@
+package testSuite.classes.conflicting_ghost_names_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.Stack")
+@Ghost("int size")
+public interface StackRefinements<E> {
+
+	public void Stack();
+
+	@StateRefinement(to="size(this) == size(old(this)) + 1")
+	public E push(E elem);
+
+	@StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1")
+	public E pop();
+
+	@StateRefinement(from="size(this) > 0")
+	public E peek();
+}

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