Update Annotations Javadocs

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

@@ -6,18 +6,17 @@
 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
+ * e.g. `@ExternalRefinementsFor("java.lang.Math")`
  *
  * @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
      */
     public String value();
 }

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

@@ -7,15 +7,18 @@
 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
+ * e.g. `@Ghost("int size")`
  *
  * @author catarina gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 @Repeatable(GhostMultiple.class)
 public @interface Ghost {
+
+    /**
+     * The type and name of the ghost variable
+     */
     public String value();
 }

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

@@ -6,12 +6,17 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to allow the creation of multiple @Ghost
+ * Annotation to allow the creation of multiple `@Ghost` annotations in a class or interface
+ * e.g. `@GhostMultiple({@Ghost("int size"), @Ghost("boolean isEmpty")})`
  *
  * @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,16 +6,22 @@
 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
+ * e.g. `@Refinement("x > 0") int x;`
  *
  * @author catarina gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.FIELD, ElementType.LOCAL_VARIABLE, ElementType.PARAMETER, ElementType.TYPE})
 public @interface Refinement {
 
+    /**
+     * The refinement string
+     */
     public String value();
 
+    /**
+     * An optional message to be included in the error message when the refinement is violated
+     */
     public String msg() default "";
 }

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

@@ -7,14 +7,18 @@
 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
+ * e.g. `@RefinementAlias("Nat(int x) { x > 0 }")`
  *
  * @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
+     */
     public String value();
 }

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

@@ -6,12 +6,17 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create a multiple Alias in a class
+ * Annotation to create multiple refinement aliases
+ * e.g. `@RefinementAliasMultiple({@RefinementAlias("Nat(int x) { x > 0 }"), @RefinementAlias("Pos(int x) { x >= 0 }")})`
  *
  * @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

@@ -6,9 +6,19 @@
 import java.lang.annotation.RetentionPolicy;
 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
+ */
 @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
+     */
     public String value();
 }

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

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

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

@@ -6,13 +6,17 @@
 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 `@StateRefinement` annotations
+ * e.g. `@StateRefinementMultiple({@StateRefinement(from="open(this)", to="closed(this)"), @StateRefinement(from="closed(this)", to="open(this)")})`
  *
  * @author catarina gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public @interface StateRefinementMultiple {
+
+    /**
+     * The array of `@StateRefinement` annotations to be created
+     */
     StateRefinement[] value();
 }

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

@@ -7,15 +7,18 @@
 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 the disjoint states in which class objects can be
+ * e.g. @StateSet({"open", "reading", "closed"})
  *
  * @author catarina gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 @Repeatable(StateSets.class)
 public @interface StateSet {
+
+    /**
+     * The array of states to be created
+     */
     public String[] value();
 }

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

@@ -6,12 +6,17 @@
 import java.lang.annotation.Target;
 
 /**
- * Interface to allow multiple StateSets in a class.
+ * Annotation to allow the creation of multiple `@StateSet` annotations
+ * e.g. `@StateSets({@StateSet({"open", "reading", "closed"}), @StateSet({"on", "off"})})`
  *
  * @author catarina gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE})
 public @interface StateSets {
+
+    /**
+     * The array of `@StateSet` annotations to be created
+     */
     StateSet[] value();
 }