Apply external contracts to inherited receiver methods

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