Check interface method bodies and calls without class-only assumptions

Fix issue #343 by resolving return contracts from the nearest method and its declaring type, including interface static and default methods. Use exact parameter types and keep lambda returns separate from enclosing methods. Add passing and failing interface regressions.

Author: CatarinaGamboa

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

@@ -0,0 +1,43 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public interface CorrectInterfaceMethodBodies {
+    static int size(String s) {
+        int n = s.length();
+        return n;
+    }
+
+    @Refinement("_ > 0")
+    static int positive() {
+        return 1;
+    }
+
+    static void checkStaticContract() {
+        @Refinement("_ > 0")
+        int n = positive();
+    }
+
+    @Refinement("_ > 0")
+    default int defaultPositive() {
+        return 1;
+    }
+
+    default CorrectInterfaceMethodBodies self() {
+        return this;
+    }
+
+    @Refinement("_ > 0")
+    default int lambdaReturnIsNotMethodReturn() {
+        java.util.function.IntSupplier supplier = () -> { return -1; };
+        return 1;
+    }
+
+    java.util.function.IntSupplier FIELD_SUPPLIER = () -> { return -1; };
+
+    @Refinement("_ > 0")
+    static int overloaded(int value) { return 1; }
+
+    @Refinement("_ < 0")
+    static int overloaded(boolean value) { return -1; }
+}

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

@@ -0,0 +1,10 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public interface ErrorInterfaceDefaultReturn {
+    @Refinement("_ > 0")
+    default int positive() {
+        return -1; // Expect: Refinement Error
+    }
+}

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

@@ -0,0 +1,11 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public interface ErrorInterfaceMethodCall {
+    static void requirePositive(@Refinement("_ > 0") int value) {}
+
+    static void badCall() {
+        requirePositive(-1); // Expect: Refinement Error
+    }
+}

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

@@ -0,0 +1,10 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public interface ErrorInterfaceStaticReturn {
+    @Refinement("_ > 0")
+    static int positive() {
+        return -1; // Expect: Refinement Error
+    }
+}

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

@@ -214,7 +214,9 @@ public <T> void visitCtNewArray(CtNewArray<T> newArray) {
     @Override
     public <T> void visitCtThisAccess(CtThisAccess<T> thisAccess) {
         super.visitCtThisAccess(thisAccess);
-        CtClass<?> c = thisAccess.getParent(CtClass.class);
+        CtType<?> c = thisAccess.getParent(CtType.class);
+        if (c == null)
+            return;
         String s = c.getSimpleName();
         if (thisAccess.getParent() instanceof CtReturn) {
             String thisName = String.format(Formats.THIS, s);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -32,6 +32,7 @@
 import spoon.reflect.declaration.CtInterface;
 import spoon.reflect.declaration.CtMethod;
 import spoon.reflect.declaration.CtParameter;
+import spoon.reflect.declaration.CtType;
 import spoon.reflect.reference.CtExecutableReference;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -188,23 +189,31 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
     }
 
     public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
-        CtClass<?> c = ret.getParent(CtClass.class);
-        String className = c.getSimpleName();
         if (ret.getReturnedExpression() == null) {
             return;
         }
 
+        // A return in a lambda belongs to that lambda, even when it is nested in a method.
+        // Looking for any enclosing CtMethod would check it against the outer method's contract.
+        CtExecutable<?> executable = ret.getParent(CtExecutable.class);
+        if (!(executable instanceof CtMethod<?> method))
+            return;
+        CtType<?> owner = method.getDeclaringType();
+        if (owner == null)
+            return;
+
         // check if there are refinements
         if (rtc.getRefinement(ret.getReturnedExpression()) == null)
             ret.getReturnedExpression().putMetadata(Keys.REFINEMENT, new Predicate());
-        CtMethod<?> method = ret.getParent(CtMethod.class);
-
         // check if method has refinements
-        if (rtc.getRefinement(method) == null || !(method.getParent() instanceof CtClass))
+        if (rtc.getRefinement(method) == null)
             return;
 
-        RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(),
-                ((CtClass<?>) method.getParent()).getQualifiedName(), method.getParameters().size());
+        List<CtTypeReference<?>> parameterTypes = new ArrayList<>();
+        for (CtParameter<?> parameter : method.getParameters())
+            parameterTypes.add(parameter.getType());
+        RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), owner.getQualifiedName(),
+                parameterTypes);
         if (fi == null)
             return;
 
@@ -214,8 +223,8 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
         }
 
         // Both return and the method have metadata
-        String thisName = String.format(Formats.THIS, className);
-        rtc.getContext().addInstanceToContext(thisName, c.getReference(), new Predicate(), ret);
+        String thisName = String.format(Formats.THIS, owner.getSimpleName());
+        rtc.getContext().addInstanceToContext(thisName, owner.getReference(), new Predicate(), ret);
 
         String returnVarName = String.format(Formats.RET, rtc.getContext().getCounter());
         Predicate cretRef = rtc.getRefinement(ret.getReturnedExpression())
@@ -241,8 +250,8 @@ public <R> void getInvocationRefinements(CtInvocation<R> invocation) throws LJEr
             if (cte != null)
                 searchMethodInLibrary(cte, invocation);
 
-        } else if (method.getParent() instanceof CtClass) {
-            String ctype = ((CtClass<?>) method.getParent()).getQualifiedName();
+        } else if (method.getParent()instanceof CtType<?> owner) {
+            String ctype = owner.getQualifiedName();
             List<CtTypeReference<?>> paramTypes = invocation.getExecutable().getParameters();
             RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, paramTypes);
             if (f != null) { // inside rtc.context