Apply external contracts to inherited receiver methods

liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/JFrameRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.inherited_external_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"displayable", "notDisplayable"})
+@ExternalRefinementsFor("javax.swing.JFrame")
+public interface JFrameRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void JFrame(String title);
+
+    @StateRefinement(to = "displayable(this)")
+    void pack();
+
+    @StateRefinement(from = "notDisplayable(this)")
+    void setUndecorated(boolean undecorated);
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/UseFrame.java

@@ -0,0 +1,11 @@
+package testSuite.classes.inherited_external_correct;
+
+import javax.swing.JFrame;
+
+public class UseFrame {
+    static void configure() {
+        JFrame frame = new JFrame("example");
+        frame.setUndecorated(true);
+        frame.pack();
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/JFrameRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.inherited_external_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"displayable", "notDisplayable"})
+@ExternalRefinementsFor("javax.swing.JFrame")
+public interface JFrameRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void JFrame(String title);
+
+    @StateRefinement(to = "displayable(this)")
+    void pack();
+
+    @StateRefinement(from = "notDisplayable(this)")
+    void setUndecorated(boolean undecorated);
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/UseFrame.java

@@ -0,0 +1,11 @@
+package testSuite.classes.inherited_external_error;
+
+import javax.swing.JFrame;
+
+public class UseFrame {
+    static void configure() {
+        JFrame frame = new JFrame("example");
+        frame.pack();
+        frame.setUndecorated(true); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Base.java

@@ -0,0 +1,7 @@
+package testSuite.classes.inherited_external_visibility.parent;
+
+public class Base {
+    private void privateMethod() {}
+    void packageMethod() {}
+    protected void protectedMethod() {}
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Child.java

@@ -0,0 +1,3 @@
+package testSuite.classes.inherited_external_visibility;
+
+public class Child extends testSuite.classes.inherited_external_visibility.parent.Base implements StaticParent {}

liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/ChildRefinements.java

@@ -0,0 +1,11 @@
+package testSuite.classes.inherited_external_visibility;
+
+import liquidjava.specification.ExternalRefinementsFor;
+
+@ExternalRefinementsFor("testSuite.classes.inherited_external_visibility.Child")
+public interface ChildRefinements {
+    void privateMethod(); // Expect: Warning
+    void packageMethod(); // Expect: Warning
+    void interfaceStatic(); // Expect: Warning
+    void protectedMethod();
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/DefaultChildRefinements.java

@@ -0,0 +1,12 @@
+import liquidjava.specification.ExternalRefinementsFor;
+
+class DefaultParent {
+    void packageMethod() {}
+}
+
+class DefaultChild extends DefaultParent {}
+
+@ExternalRefinementsFor("DefaultChild")
+public interface DefaultChildRefinements {
+    void packageMethod();
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/StaticParent.java

@@ -0,0 +1,5 @@
+package testSuite.classes.inherited_external_visibility;
+
+public interface StaticParent {
+    static void interfaceStatic() {}
+}

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

@@ -0,0 +1,11 @@
+package testSuite.classes.inherited_overload_correct;
+
+import liquidjava.specification.*;
+
+@ExternalRefinementsFor("java.util.Stack")
+@StateSet({"ready", "changed"})
+public interface StackRefinements<E> {
+    @StateRefinement(to = "ready(this)") void Stack();
+    @StateRefinement(to = "changed(this)") E remove(int index);
+    @StateRefinement(from = "ready(this)") E peek();
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/UseStack.java

@@ -0,0 +1,12 @@
+package testSuite.classes.inherited_overload_correct;
+
+import java.util.Stack;
+
+public class UseStack {
+    static void check() {
+        Stack<String> stack = new Stack<>();
+        stack.add("value");
+        stack.remove("value");
+        stack.peek();
+    }
+}

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

@@ -0,0 +1,11 @@
+package testSuite.classes.inherited_overload_error;
+
+import liquidjava.specification.*;
+
+@ExternalRefinementsFor("java.util.Stack")
+@StateSet({"ready", "changed"})
+public interface StackRefinements<E> {
+    @StateRefinement(to = "ready(this)") void Stack();
+    @StateRefinement(to = "changed(this)") E remove(int index);
+    @StateRefinement(from = "ready(this)") E peek();
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/UseStack.java

@@ -0,0 +1,12 @@
+package testSuite.classes.inherited_overload_error;
+
+import java.util.Stack;
+
+public class UseStack {
+    static void check() {
+        Stack<String> stack = new Stack<>();
+        stack.add("value");
+        stack.remove(0);
+        stack.peek(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Base.java

@@ -0,0 +1,9 @@
+package testSuite.classes.inherited_source_correct;
+
+public class Base {
+    public void change(int value) {}
+    public void change(String value) {}
+    public void use() {}
+    public void inheritedPositive(@liquidjava.specification.Refinement("_ > 0") int value) {}
+    public void overridePositive(@liquidjava.specification.Refinement("_ > 0") int value) {}
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Child.java

@@ -0,0 +1,6 @@
+package testSuite.classes.inherited_source_correct;
+
+public class Child extends Base {
+    @Override
+    public void overridePositive(@liquidjava.specification.Refinement("_ >= 0") int value) {}
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/ChildRefinements.java

@@ -0,0 +1,11 @@
+package testSuite.classes.inherited_source_correct;
+
+import liquidjava.specification.*;
+
+@ExternalRefinementsFor("testSuite.classes.inherited_source_correct.Child")
+@StateSet({"ready", "changed"})
+public interface ChildRefinements {
+    @StateRefinement(to = "ready(this)") void Child();
+    @StateRefinement(to = "changed(this)") void change(int value);
+    @StateRefinement(from = "ready(this)") void use();
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/UseChild.java

@@ -0,0 +1,17 @@
+package testSuite.classes.inherited_source_correct;
+
+public class UseChild {
+    static void check() {
+        Child child = new Child();
+        child.change("unchanged");
+        child.use();
+    }
+
+    static void superclassFallback() {
+        new Child().inheritedPositive(1);
+    }
+
+    static void subclassOverride() {
+        new Child().overridePositive(0);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Base.java

@@ -0,0 +1,9 @@
+package testSuite.classes.inherited_source_error;
+
+public class Base {
+    public void change(int value) {}
+    public void change(String value) {}
+    public void use() {}
+    public void inheritedPositive(@liquidjava.specification.Refinement("_ > 0") int value) {}
+    public void overridePositive(@liquidjava.specification.Refinement("_ > 0") int value) {}
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Child.java

@@ -0,0 +1,6 @@
+package testSuite.classes.inherited_source_error;
+
+public class Child extends Base {
+    @Override
+    public void overridePositive(@liquidjava.specification.Refinement("_ >= 0") int value) {}
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/ChildRefinements.java

@@ -0,0 +1,11 @@
+package testSuite.classes.inherited_source_error;
+
+import liquidjava.specification.*;
+
+@ExternalRefinementsFor("testSuite.classes.inherited_source_error.Child")
+@StateSet({"ready", "changed"})
+public interface ChildRefinements {
+    @StateRefinement(to = "ready(this)") void Child();
+    @StateRefinement(to = "changed(this)") void change(int value);
+    @StateRefinement(from = "ready(this)") void use();
+}

liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/UseChild.java

@@ -0,0 +1,17 @@
+package testSuite.classes.inherited_source_error;
+
+public class UseChild {
+    static void check() {
+        Child child = new Child();
+        child.change(1);
+        child.use(); // Expect: State Refinement Error
+    }
+
+    static void superclassFallback() {
+        new Child().inheritedPositive(-1); // Expect: Refinement Error
+    }
+
+    static void subclassOverride() {
+        new Child().overridePositive(0);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

@@ -344,12 +344,18 @@ public RefinedFunction getFunction(String name, String target, int size) {
     }
 
     public RefinedFunction getFunction(String name, String target, List<CtTypeReference<?>> paramTypes) {
+        RefinedFunction exact = getFunctionExact(name, target, paramTypes);
+        return exact != null ? exact : getFunction(name, target, paramTypes.size());
+    }
+
+    /** Looks up a receiver-specific contract without selecting a different overload by arity. */
+    public RefinedFunction getFunctionExact(String name, String target, List<CtTypeReference<?>> paramTypes) {
         for (RefinedFunction fi : ctxFunctions) {
             if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target)
                     && argumentTypesMatch(fi.getArguments(), paramTypes))
                 return fi;
         }
-        return getFunction(name, target, paramTypes.size());
+        return null;
     }
 
     private boolean argumentTypesMatch(List<Variable> args, List<CtTypeReference<?>> paramTypes) {

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

@@ -2,6 +2,7 @@
 
 import java.util.List;
 import java.util.Optional;
+import java.util.stream.Stream;
 
 import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.LJError;
@@ -140,11 +141,36 @@ private boolean classExists(String className) {
 
     private boolean methodExists(CtType<?> targetType, CtMethod<?> method) {
         // find method with matching signature
-        return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName()))
+        return inheritedMethods(targetType).filter(m -> m.getSimpleName().equals(method.getSimpleName()))
                 .anyMatch(m -> parametersMatch(m.getParameters(), method.getParameters())
                         && typesMatch(m.getType(), method.getType()));
     }
 
+    /** Includes only methods that are declared on, or inherited by, the external target. */
+    private Stream<CtMethod<?>> inheritedMethods(CtType<?> targetType) {
+        return targetType.getAllMethods().stream().filter(method -> {
+            CtType<?> owner = method.getDeclaringType();
+            if (owner == null)
+                return false;
+            if (owner.getQualifiedName().equals(targetType.getQualifiedName()))
+                return true;
+            if (method.isPrivate() || owner instanceof CtInterface<?> && method.isStatic())
+                return false;
+            if (method.isPublic() || method.isProtected())
+                return true;
+            // A package-private method stops being inherited when a superclass crosses package boundaries.
+            CtType<?> current = targetType;
+            while (current != null && !current.getQualifiedName().equals(owner.getQualifiedName())) {
+                if (current.getPackage() == null || owner.getPackage() == null
+                        || !current.getPackage().getQualifiedName().equals(owner.getPackage().getQualifiedName()))
+                    return false;
+                CtTypeReference<?> parent = current.getSuperclass();
+                current = parent == null ? null : parent.getTypeDeclaration();
+            }
+            return current != null;
+        });
+    }
+
     private boolean constructorExists(CtType<?> targetType, CtMethod<?> method) {
         // find constructor with matching signature
         CtClass<?> targetClass = (CtClass<?>) targetType;
@@ -188,7 +214,7 @@ private boolean parametersMatch(List<?> targetParams, List<?> refinementParams)
     }
 
     private String[] getOverloads(CtType<?> targetType, CtMethod<?> method) {
-        return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName()))
+        return inheritedMethods(targetType).filter(m -> m.getSimpleName().equals(method.getSimpleName()))
                 .map(m -> String.format("%s %s", m.getType().getSimpleName(), m.getSignature())).toArray(String[]::new);
     }
 }

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

@@ -233,6 +233,8 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
     // ################################
 
     public <R> void getInvocationRefinements(CtInvocation<R> invocation) throws LJError {
+        if (tryReceiverRefinements(invocation))
+            return;
         CtExecutable<?> method = invocation.getExecutable().getDeclaration();
         if (method == null) {
 
@@ -252,6 +254,23 @@ public <R> void getInvocationRefinements(CtInvocation<R> invocation) throws LJEr
         }
     }
 
+    private boolean tryReceiverRefinements(CtInvocation<?> invocation) throws LJError {
+        CtExpression<?> receiver = invocation.getTarget();
+        if (receiver == null || receiver.getType() == null)
+            return false;
+        String receiverType = receiver.getType().getQualifiedName();
+        CtExecutableReference<?> executable = invocation.getExecutable();
+        for (String key : List.of(Utils.qualifyName(receiverType, executable.getSignature()), executable.getSignature(),
+                executable.getSimpleName(), Utils.qualifyName(receiverType, executable.getSimpleName()))) {
+            if (rtc.getContext().getFunctionExact(key, receiverType, executable.getParameters()) != null) {
+                checkInvocationRefinements(invocation, invocation.getArguments(), receiver, key, receiverType,
+                        executable.getParameters());
+                return true;
+            }
+        }
+        return false;
+    }
+
     private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?> invocation) throws LJError {
         CtTypeReference<?> ctref = ctr.getDeclaringType();
         if (ctref == null) {