Verify static and default interface method bodies

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