Merge

Author: rcosta358

README.md

@@ -52,7 +52,7 @@ Additionally, you'll need the following dependency, which includes the LiquidJav
 <dependency>
     <groupId>io.github.liquid-java</groupId>
     <artifactId>liquidjava-api</artifactId>
-    <version>0.0.4</version>
+    <version>0.0.5</version>
 </dependency>
 ```
 
@@ -63,7 +63,7 @@ repositories {
 }
 
 dependencies {
-    implementation 'io.github.liquid-java:liquidjava-api:0.0.4'
+    implementation 'io.github.liquid-java:liquidjava-api:0.0.5'
 }
 ```
 

liquidjava-api/pom.xml

@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-api</artifactId>
-	<version>0.0.4</version>
+	<version>0.0.5</version>
 	<name>liquidjava-api</name>
 	<description>LiquidJava API</description>
 	<url>https://github.com/liquid-java/liquidjava</url>

liquidjava-api/src/main/java/liquidjava/specification/Ghost.java

@@ -26,7 +26,7 @@
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
-@Repeatable(GhostMultiple.class)
+@Repeatable(Ghost.Multiple.class)
 public @interface Ghost {
 
     /**
@@ -40,4 +40,13 @@
      * </pre>
      */
     String value();
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple ghost declarations.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.TYPE})
+    @interface Multiple {
+        Ghost[] value();
+    }
 }

liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java

@@ -28,7 +28,7 @@
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
-@Repeatable(RefinementAliasMultiple.class)
+@Repeatable(RefinementAlias.Multiple.class)
 public @interface RefinementAlias {
 
     /**
@@ -42,4 +42,13 @@
      * </pre>
      */
     String value();
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple refinement aliases.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.TYPE})
+    @interface Multiple {
+        RefinementAlias[] value();
+    }
 }

liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java

@@ -7,17 +7,18 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation that allows the creation of ghost variables or refinement aliases within method or constructor scope.
+ * Annotation that allows the creation of custom ghost functions within classes or interfaces.
  * <p>
- * This annotation enables the declaration of ghosts and refinement aliases.
+ * This annotation enables the declaration of custom ghost functions.
  * <p>
  * <strong>Example:</strong>
  * <pre>
  * {@code
- * @RefinementPredicate("ghost int size")
- * @RefinementPredicate("type Nat(int x) { x > 0 }")
- * public void process() {
- *     // ...
+ * @RefinementPredicate("int totalPrice(Order o)")
+ * public class Order {
+ *     @StateRefinement(to = "totalPrice(this) == 0")
+ *     public Order() {
+ *     }
  * }
  * }
  * </pre>
@@ -27,20 +28,28 @@
  * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
-@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
-@Repeatable(RefinementPredicateMultiple.class)
+@Target({ElementType.TYPE})
+@Repeatable(RefinementPredicate.Multiple.class)
 public @interface RefinementPredicate {
 
     /**
-     * The refinement predicate string, which can define a ghost variable or a refinement alias.
+     * The refinement predicate string, which defines a ghost function declaration.
      * <p>
      * <strong>Example:</strong>
      * <pre>
      * {@code
-     * @RefinementPredicate("ghost int size")
-     * @RefinementPredicate("type Nat(int x) { x > 0 }")
+     * @RefinementPredicate("int totalPrice(Order o)")
      * }
      * </pre>
      */
     String value();
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple refinement predicates.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.TYPE})
+    @interface Multiple {
+        RefinementPredicate[] value();
+    }
 }

liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java

@@ -28,7 +28,7 @@
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
-@Repeatable(StateRefinementMultiple.class)
+@Repeatable(StateRefinement.Multiple.class)
 public @interface StateRefinement {
 
     /**
@@ -66,4 +66,13 @@
      * </pre>
      */
     String msg() default "";
+
+    /**
+     * Container annotation used by {@link Repeatable} to support multiple state transitions.
+     */
+    @Retention(RetentionPolicy.RUNTIME)
+    @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+    @interface Multiple {
+        StateRefinement[] value();
+    }
 }