Add DefaultMutableTreeNode Refinements

rcosta358 · rcosta358 · commit 4f90e6d63b6c · 2026-02-02T14:38:16.000Z
diff --git a/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeRefinements.java b/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeRefinements.java
@@ -0,0 +1,47 @@
+package com.defaultMutableTreeNode;
+
+import javax.swing.tree.MutableTreeNode;
+import javax.swing.tree.TreeNode;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@RefinementAlias("Positive(int i) { i >= 0 }")
+@ExternalRefinementsFor("javax.swing.tree.DefaultMutableTreeNode")
+@StateSet({"childrenAllowed", "childrenNotAllowed"})
+public interface DefaultMutableTreeNodeRefinements {
+    
+    @StateRefinement(to="childrenAllowed(this)")
+    public void DefaultMutableTreeNode();
+
+    @StateRefinement(to="childrenAllowed(this)")
+    public void DefaultMutableTreeNode(Object userObject);
+
+    @StateRefinement(to="allowsChildren ? childrenAllowed(this) : childrenNotAllowed(this)")
+    public void DefaultMutableTreeNode(Object userObject, boolean allowsChildren);
+
+    @StateRefinement(from="childrenAllowed(this)")
+    public void insert(MutableTreeNode newChild, @Refinement("Positive(_)") int childIndex);
+
+    @StateRefinement(from="childrenAllowed(this)")
+    public void add(MutableTreeNode newChild);
+
+    @StateRefinement(to="allows ? childrenAllowed(this) : childrenNotAllowed(this)")
+    public void setAllowsChildren(boolean allows);
+
+    @Refinement("childrenAllowed(this) ? true : false")
+    public boolean getAllowsChildren();
+
+    public void remove(@Refinement("Positive(_)") int childIndex);
+
+    public TreeNode getChildAt(@Refinement("Positive(_)") int index);
+
+    @Refinement("Positive(_)")
+    public int getChildCount();
+
+    @Refinement("Positive(_) || _ == -1")
+    public int getIndex(TreeNode aChild);
+}
diff --git a/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeTests.java b/examples/demo/src/main/java/com/defaultMutableTreeNode/DefaultMutableTreeNodeTests.java
@@ -0,0 +1,30 @@
+package com.defaultMutableTreeNode;
+
+import javax.swing.tree.DefaultMutableTreeNode;
+
+public class DefaultMutableTreeNodeTests {
+    
+    public void testOk() {
+        DefaultMutableTreeNode node = new DefaultMutableTreeNode();
+        node.insert(null, 0);
+        node.getIndex(null);
+        node.remove(0);
+    }
+
+    public void testAddUnwantedChildConstructor() {
+        DefaultMutableTreeNode node = new DefaultMutableTreeNode(null, false);
+        node.insert(null, 0); // error
+    }
+
+    public void testAddUnwantedChildSetter() {
+        DefaultMutableTreeNode node = new DefaultMutableTreeNode(null, true);
+        node.insert(null, 0);
+        node.setAllowsChildren(false);
+        node.add(null); // error
+    }
+
+    public void testAddChildInvalidIndex() {
+        DefaultMutableTreeNode node = new DefaultMutableTreeNode();
+        node.insert(null, -1); // error
+    }
+}
