Merge branch 'main' into feature-result-refinement

Author: rajshivu

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.3</version>
+    <version>0.0.4</version>
 </dependency>
 ```
 
@@ -63,7 +63,7 @@ repositories {
 }
 
 dependencies {
-    implementation 'io.github.liquid-java:liquidjava-api:0.0.3'
+    implementation 'io.github.liquid-java:liquidjava-api:0.0.4'
 }
 ```
 

liquidjava-api/pom.xml

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

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

@@ -6,18 +6,37 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create refinements for an external library. The annotation receives the path of the
- * library e.g. @ExternalRefinementsFor("java.lang.Math")
+ * Annotation to refine a class or interface of an external library.
+ * <p>
+ * This annotation allows you to specify refinements and state transitions for classes from external libraries
+ * that you cannot directly annotate. The refinements apply to all instances of the specified class.
+ * <p>
+ * <strong>Example:</strong>
+ * <pre>
+ * {@code
+ * @ExternalRefinementsFor("java.lang.Math")
+ * public interface MathRefinements {
+ *     @Refinement("_ >= 0")
+ *     public double sqrt(double x);
+ * }
+ * }
+ * </pre>
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 public @interface ExternalRefinementsFor {
+    
     /**
-     * The prefix of the external method
-     *
-     * @return
+     * The fully qualified name of the class or interface for which the refinements are being defined.
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @ExternalRefinementsFor("java.lang.Math")
+     * }
+     * </pre>
      */
-    public String value();
+    String value();
 }

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

@@ -7,15 +7,37 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create a ghost variable for a class. The annotation receives
- * the type and name of
- * the ghost within a string e.g. @Ghost("int size")
+ * Annotation to create a ghost variable for a class or interface.
+ * <p>
+ * Ghost variables that only exist during the verification and can be used in refinements and state refinements.
+ * They are not part of the actual implementation but help specify behavior and invariants.
+ * <p>
+ * <strong>Example:</strong>
+ * <pre>
+ * {@code
+ * @Ghost("int size")
+ * public class MyStack {
+ *     // ...
+ * }
+ * }
+ * </pre>
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 @Repeatable(GhostMultiple.class)
 public @interface Ghost {
-    public String value();
+
+    /**
+     * The type and name of the ghost variable.
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @Ghost("int size")
+     * }
+     * </pre>
+     */
+    String value();
 }

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

@@ -6,9 +6,9 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to allow the creation of multiple @Ghost
+ * Annotation to allow the creation of multiple ghost variables.
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})

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

@@ -6,14 +6,49 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to add a refinement to variables, class fields, method's parameters and method's
- * return value e.g. @Refinement("x > 0") int x;
+ * Annotation to add a refinement to variables, class fields, method's parameters and method's return values.
+ * <p>
+ * Refinements are logical predicates that must hold for the annotated element.
+ * <p>
+ * <strong>Example:</strong>
+ * <pre>
+ * {@code
+ * @Refinement("x > 0")
+ * int x;
+ * 
+ * @Refinement("_ > 0")
+ * int increment(@Refinement("_ >= 0") int n) {
+ *     return n + 1;
+ * }
+ * </pre>
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.FIELD, ElementType.LOCAL_VARIABLE, ElementType.PARAMETER, ElementType.TYPE})
 public @interface Refinement {
 
-    public String value();
+    /**
+     * The refinement string that defines a logical predicate that must hold for the annotated element.
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @Refinement("x > 0")
+     * }
+     * </pre>
+     */
+    String value();
+
+    /**
+     * Custom error message to be shown when the refinement is violated (optional).
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @Refinement(value = "x > 0", msg = "x must be positive")
+     * }
+     * </pre>
+     */
+    String msg() default "";
 }

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

@@ -7,14 +7,39 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create a ghost variable for a class. The annotation receives the type and name of
- * the ghost within a string e.g. @RefinementAlias("Nat(int x) {x > 0}")
+ * Annotation to create a refinement alias to be reused in refinements.
+ * <p>
+ * Refinement aliases can be used to define reusable refinement predicates with parameters.
+ * They help reduce duplication and improve readability of complex refinement specifications.
+ * <p>
+ * <strong>Example:</strong>
+ * <pre>
+ * {@code
+ * @RefinementAlias("Nat(int x) { x > 0 }")
+ * public class MyClass {
+ *     @Refinement("Nat(_)")
+ *     int value;
+ * }
+ * }
+ * </pre>
  *
- * @author catarina gamboa
+ * @see Refinement
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 @Repeatable(RefinementAliasMultiple.class)
 public @interface RefinementAlias {
-    public String value();
+
+    /**
+     * The refinement alias string, which includes the name of the alias, its parameters and the refinement itself.
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @RefinementAlias("Nat(int x) { x > 0 }")
+     * }
+     * </pre>
+     */
+    String value();
 }

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

@@ -6,9 +6,9 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create a multiple Alias in a class
+ * Annotation to create multiple refinement aliases.
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})

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

@@ -6,9 +6,41 @@
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
+/**
+ * Annotation that allows the creation of ghost variables or refinement aliases within method or constructor scope.
+ * <p>
+ * This annotation enables the declaration of ghosts and refinement aliases.
+ * <p>
+ * <strong>Example:</strong>
+ * <pre>
+ * {@code
+ * @RefinementPredicate("ghost int size")
+ * @RefinementPredicate("type Nat(int x) { x > 0 }")
+ * public void process() {
+ *     // ...
+ * }
+ * }
+ * </pre>
+ *
+ * @see Ghost
+ * @see RefinementAlias
+ * @author Catarina Gamboa
+ */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 @Repeatable(RefinementPredicateMultiple.class)
 public @interface RefinementPredicate {
-    public String value();
+
+    /**
+     * The refinement predicate string, which can define a ghost variable or a refinement alias.
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @RefinementPredicate("ghost int size")
+     * @RefinementPredicate("type Nat(int x) { x > 0 }")
+     * }
+     * </pre>
+     */
+    String value();
 }

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

@@ -5,6 +5,11 @@
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
+/**
+ * Annotation to allow the creation of multiple refinement predicates.
+ *
+ * @author Catarina Gamboa
+ */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public @interface RefinementPredicateMultiple {