Update Annotations Javadocs

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,16 +6,50 @@
 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")
+ * public int getSize() {
+ *     // ...
+ * }
+ * }
+ * </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();
 
-    public String msg() default "";
+    /**
+     * 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 {

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

@@ -7,20 +7,63 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create state transitions in a method. The annotation has three arguments: from : the
- * state in which the object needs to be for the method to be invoked correctly to : the state in
- * which the object will be after the execution of the method msg : optional custom error message to display when refinement is violated
- * e.g. @StateRefinement(from="open(this)", to="closed(this)")
+ * Annotation to create state transitions in a method using states defined in state sets.
+ * <p>
+ * This annotation specifies the required precondition state and the resulting
+ * postcondition state when a method or constructor is invoked.
+ * Constructors can only specify the postcondition state since they create a new object.
+ * <p>
+ * <strong>Example:</strong>
+ * <pre>
+ * {@code
+ * @StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")
+ * public void close() {
+ *     // ...
+ * }
+ * }
+ * </pre>
  *
- * @author catarina gamboa
+ * @see StateSet
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 @Repeatable(StateRefinementMultiple.class)
 public @interface StateRefinement {
-    public String from() default "";
 
-    public String to() default "";
+    /**
+     * The logical pre-condition that defines the state in which the object needs to be before calling the method (optional)
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @StateRefinement(from="open(this)")
+     * }
+     * </pre>
+     */
+    String from() default "";
 
-    public String msg() default "";
+    /**
+     * The logical post-condition that defines the state in which the object will be after calling the method (optional)
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @StateRefinement(from="open(this)", to="closed(this)")
+     * }
+     * </pre>
+     */
+    String to() default "";
+
+    /**
+     * Custom error message to be shown when the {@code from} pre-condition is violated (optional)
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")
+     * }
+     * </pre>
+     */
+    String msg() default "";
 }

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

@@ -6,10 +6,9 @@
 import java.lang.annotation.Target;
 
 /**
- * Interface to allow multiple state refinements in a method. A method can have a state refinement
- * for each set of different source and destination states
+ * Annotation to allow the creation of multiple state transitions.
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})

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

@@ -7,15 +7,35 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create the disjoint states in which class objects can be. The annotation receives a
- * list of strings representing the names of the states. e.g. @StateSet({"open", "reading",
- * "closed"})
+ * Annotation to create a set of disjoint states in which class objects can be.
+ * <p>
+ * An object will always be in exactly one state from each state set at any given time,
+ * and cannot be in more than one state from the same state set (e.g., {@code open} and {@code closed} simultaneously).
+ * To allow an object to be in multiple states at once, they must be from different state sets.
+ * <p>
+ * <strong>Example:</strong>
+ * <pre>
+ * {@code
+ * @StateSet({"open", "reading", "closed"}})
+ * </pre>
  *
- * @author catarina gamboa
+ * @see StateRefinement
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 @Repeatable(StateSets.class)
 public @interface StateSet {
-    public String[] value();
+
+    /**
+     * The array of states to be created.
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @StateSet({"open", "reading", "closed"})
+     * }
+     * </pre>
+     */
+    String[] value();
 }