Apply external contracts to inherited receiver methods (#387)

An external specification for `JFrame` could not name inherited `pack()`
or `setUndecorated(boolean)`. Both declarations produced warnings, and
`pack(); setUndecorated(true);` incorrectly passed verification.

Validate external method signatures and overload suggestions against
methods the target actually inherits. Exclude private ancestor methods,
interface static methods, and package-private methods lost across
package boundaries. Resolve invocation contracts against the receiver's
static type first, using exact parameter types to prevent equal-arity
overload collisions, then retain the existing declaring-type lookup.
This applies to both library calls and resolved source method calls.

Add paired JFrame protocol, source inheritance, and JDK overload
regressions, plus superclass fallback, subclass override, and inherited
visibility coverage.

Validation: `mvn -pl liquidjava-verifier test` — 394 tests, zero
failures/errors. Targeted checks also verified the exact JFrame state
error, both overload paths, and exactly three visibility warnings while
accepting inherited protected and default-package methods.

Adversarial and devil’s advocate review identified two implementation
traps covered here: the existing typed context lookup falls back to
arity, and Spoon’s complete method set includes non-inherited
private/interface-static/package-private declarations. Receiver lookup
uses a new exact API; inherited validation filters those declarations.

Closes #379.

Author: CatarinaGamboa

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