allow interfaces to be also annotated with external refinements

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/iterator_interface_correct/IteratorRefinements.java

@@ -0,0 +1,23 @@
+package testSuite.classes.iterator_interface_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+/**
+ * External refinements for the JDK interface {@code java.util.Iterator}. Exercises {@code @ExternalRefinementsFor} on an
+ * interface target (not a concrete class) and a generic method ({@code N next()} vs the JDK's {@code E next()}).
+ */
+@StateSet({ "hasMore", "inNext", "notInNext" })
+@ExternalRefinementsFor("java.util.Iterator")
+public interface IteratorRefinements<N> {
+
+    @StateRefinement(to = "_ --> hasMore()")
+    boolean hasNext();
+
+    @StateRefinement(from = "hasMore()", to = "inNext()")
+    N next();
+
+    @StateRefinement(from = "inNext()", to = "notInNext()")
+    void remove();
+}

liquidjava-example/src/main/java/testSuite/classes/iterator_interface_correct/Test.java

@@ -0,0 +1,17 @@
+package testSuite.classes.iterator_interface_correct;
+
+import java.util.ArrayList;
+import java.util.Iterator;
+
+public class Test {
+
+    public static void main(String[] args) {
+        ArrayList<Object> list = new ArrayList<>();
+        list.add(new Object());
+        Iterator<Object> it = list.iterator();
+        if (it.hasNext()) {
+            it.next();
+            it.remove(); // valid: remove() after next()
+        }
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/iterator_interface_error/IteratorRefinements.java

@@ -0,0 +1,23 @@
+package testSuite.classes.iterator_interface_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+/**
+ * External refinements for the JDK interface {@code java.util.Iterator}. Exercises {@code @ExternalRefinementsFor} on an
+ * interface target (not a concrete class) and a generic method ({@code N next()} vs the JDK's {@code E next()}).
+ */
+@StateSet({ "hasMore", "inNext", "notInNext" })
+@ExternalRefinementsFor("java.util.Iterator")
+public interface IteratorRefinements<N> {
+
+    @StateRefinement(to = "_ --> hasMore()")
+    boolean hasNext();
+
+    @StateRefinement(from = "hasMore()", to = "inNext()")
+    N next();
+
+    @StateRefinement(from = "inNext()", to = "notInNext()")
+    void remove();
+}

liquidjava-example/src/main/java/testSuite/classes/iterator_interface_error/Test.java

@@ -0,0 +1,14 @@
+package testSuite.classes.iterator_interface_error;
+
+import java.util.ArrayList;
+import java.util.Iterator;
+
+public class Test {
+
+    public static void main(String[] args) {
+        ArrayList<Object> list = new ArrayList<>();
+        list.add(new Object());
+        Iterator<Object> it = list.iterator();
+        it.remove(); // State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java

@@ -24,6 +24,7 @@
 import spoon.reflect.declaration.CtParameter;
 import spoon.reflect.declaration.CtType;
 import spoon.reflect.factory.Factory;
+import spoon.reflect.reference.CtTypeParameterReference;
 import spoon.reflect.reference.CtTypeReference;
 
 public class ExternalRefinementTypeChecker extends TypeChecker {
@@ -66,10 +67,13 @@ public <T> void visitCtField(CtField<T> f) {
 
     public <R> void visitCtMethod(CtMethod<R> method) {
         CtType<?> targetType = factory.Type().createReference(prefix).getTypeDeclaration();
-        if (!(targetType instanceof CtClass))
+        if (!(targetType instanceof CtClass) && !(targetType instanceof CtInterface))
             return;
 
-        boolean isConstructor = method.getSimpleName().equals(targetType.getSimpleName());
+        // Interfaces have no constructors; only a class can declare one, so the constructor-name shortcut
+        // (a refinement method named like the target type) only applies to class targets.
+        boolean isConstructor = targetType instanceof CtClass
+                && method.getSimpleName().equals(targetType.getSimpleName());
         if (isConstructor) {
             if (!constructorExists(targetType, method)) {
                 String signature = method.getSignature();
@@ -149,6 +153,12 @@ private boolean typesMatch(CtTypeReference<?> type1, CtTypeReference<?> type2) {
         if (type1 == null || type2 == null)
             return false;
 
+        // Type variables (generics such as E, N, T) carry different names in the JDK type and in the refinement
+        // interface (e.g. Iterator's `E next()` vs a spec's `N next()`), so they never match by qualified name.
+        // Treat any two type-parameter references as compatible.
+        if (type1 instanceof CtTypeParameterReference && type2 instanceof CtTypeParameterReference)
+            return true;
+
         return type1.getQualifiedName().equals(type2.getQualifiedName());
     }