Merge branch 'main' into claude/increase-test-coverage-011CV6ApkFZRxiQKNWjPW52w

Author: rcosta358

.gitattributes

@@ -0,0 +1 @@
+* text=auto eol=lf

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java

@@ -0,0 +1,8 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.StateSet;
+
+@StateSet({"Open", "Closed"})
+public class CustomError {
+    
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int size")
+public class GhostInvocationError {
+
+    @StateRefinement(to="size(this, this) == 0")
+    public void test() {}
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class IllegalConstructorTransitionError {
+
+    @StateRefinement(from="open(this)", to="closed(this)")
+    public IllegalConstructorTransitionError() {}
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java

@@ -0,0 +1,10 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Refinement;
+
+public class InvalidRefinementError {
+    public static void main(String[] args) {
+        @Refinement("_ + 1")
+        int x = 5;
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Refinement;
+
+public class NotFoundError {
+
+    public static void main(String[] args) {
+        @Refinement("x > 0")
+        int y = 1;
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Refinement;
+
+public class RefinementError {
+    
+    public static void main(String[] args) {
+        @Refinement("x > 0")
+        int x = -1;
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java

@@ -0,0 +1,14 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class StateConflictError {
+    
+    @StateRefinement(to="open(this)")
+    public StateConflictError() {}
+
+    @StateRefinement(from="open(this) && closed(this)")
+    public void close() {}
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java

@@ -0,0 +1,20 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class StateRefinementError {
+    
+    @StateRefinement(to="open(this)")
+    public StateRefinementError() {}
+
+    @StateRefinement(from="!closed(this)", to="closed(this)")
+    public void close() {}
+
+    public static void main(String[] args) {
+        StateRefinementError s = new StateRefinementError();
+        s.close();
+        s.close();
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/SyntaxError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Refinement;
+
+public class SyntaxError {
+    
+    public static void main(String[] args) {
+        @Refinement("x $ 0")
+        int x = -1;
+    }
+}