Improve Javadocs

Author: rcosta358

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

@@ -6,17 +6,37 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to refine a class or interface of an external 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 fully qualified name of the class or interface for which the refinements are being defined
+     * 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,18 +7,37 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create a ghost variable for a class or interface
- * 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 {
 
     /**
-     * The type and name of the ghost variable
+     * The type and name of the ghost variable.
+     * <p>
+     * <strong>Example:</strong>
+     * <pre>
+     * {@code
+     * @Ghost("int size")
+     * }
+     * </pre>
      */
-    public String value();
+    String value();
 }

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

@@ -6,17 +6,12 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to allow the creation of multiple `@Ghost` annotations in a class or interface
- * e.g. `@GhostMultiple({@Ghost("int size"), @Ghost("boolean isEmpty")})`
+ * Annotation to allow the creation of multiple ghost variables.
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 public @interface GhostMultiple {
-
-    /**
-     * The array of `@Ghost` annotations to be created
-     */
     Ghost[] value();
 }

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

@@ -6,22 +6,50 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to add a refinement to variables, class fields, method's parameters and method's return values
- * 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 {
 
     /**
-     * The refinement string
+     * 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>
      */
-    public String value();
+    String value();
 
     /**
-     * An optional message to be included in the error message when the refinement is violated
+     * 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>
      */
-    public String msg() default "";
+    String msg() default "";
 }

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

@@ -7,18 +7,39 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create a refinement alias
- * 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 {
 
     /**
-     * The refinement alias string, which includes the name of the alias, its parameters and the refinement itself
+     * 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>
      */
-    public String value();
+    String value();
 }

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

@@ -6,17 +6,12 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create multiple refinement aliases
- * e.g. `@RefinementAliasMultiple({@RefinementAlias("Nat(int x) { x > 0 }"), @RefinementAlias("Pos(int x) { x >= 0 }")})`
+ * Annotation to create multiple refinement aliases.
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 public @interface RefinementAliasMultiple {
-
-    /**
-     * The array of `@RefinementAlias` annotations to be created
-     */
     RefinementAlias[] value();
 }

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

@@ -7,18 +7,40 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation that allows the creation of ghosts or refinement aliases
- * e.g. `@RefinementPredicate("ghost int size")`, `@RefinementPredicate("type Nat(int x) { x > 0 }")`
- * 
- * @author catarina gamboa
+ * 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 {
 
     /**
-     * The refinement predicate string, which can define a ghost variable or a refinement alias
+     * 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>
      */
-    public String value();
+    String value();
 }

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

@@ -6,17 +6,12 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to allow the creation of multiple `@RefinementPredicate` annotations
- * e.g. `@RefinementPredicateMultiple({`@RefinementPredicate("ghost int size")`, `@RefinementPredicate("type Nat(int x) { x > 0 }")`})`
+ * Annotation to allow the creation of multiple refinement predicates.
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public @interface RefinementPredicateMultiple {
-
-    /**
-     * The array of `@RefinementPredicate` annotations to be created
-     */
     RefinementPredicate[] value();
 }

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

@@ -7,28 +7,63 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create state transitions in a method
- * e.g. `@StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")`
+ * 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 {
 
     /**
-     * The state in which the object needs to be before calling the method
+     * 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>
      */
-    public String from() default "";
+    String from() default "";
 
     /**
-     * The state in which the object will be after calling the method
+     * 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>
      */
-    public String to() default "";
+    String to() default "";
 
     /**
-     * Optional custom error message to be included in the error message when the `from` is violated
+     * 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>
      */
-    public String msg() default "";
+    String msg() default "";
 }

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

@@ -6,17 +6,12 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to allow the creation of multiple `@StateRefinement` annotations
- * e.g. `@StateRefinementMultiple({@StateRefinement(from="open(this)", to="closed(this)"), @StateRefinement(from="closed(this)", to="open(this)")})`
+ * Annotation to allow the creation of multiple state transitions.
  *
- * @author catarina gamboa
+ * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public @interface StateRefinementMultiple {
-
-    /**
-     * The array of `@StateRefinement` annotations to be created
-     */
     StateRefinement[] value();
 }