From 0fd494d706eabc62f3bd86c902cd113ed6e40d45 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Feb 2026 16:50:57 +0000 Subject: [PATCH 1/2] Update Annotations Javadocs --- .../specification/ExternalRefinementsFor.java | 9 ++++----- .../java/liquidjava/specification/Ghost.java | 9 ++++++--- .../liquidjava/specification/GhostMultiple.java | 7 ++++++- .../liquidjava/specification/Refinement.java | 10 ++++++++-- .../specification/RefinementAlias.java | 8 ++++++-- .../specification/RefinementAliasMultiple.java | 7 ++++++- .../specification/RefinementPredicate.java | 10 ++++++++++ .../RefinementPredicateMultiple.java | 10 ++++++++++ .../specification/StateRefinement.java | 16 ++++++++++++---- .../specification/StateRefinementMultiple.java | 8 ++++++-- .../java/liquidjava/specification/StateSet.java | 9 ++++++--- .../java/liquidjava/specification/StateSets.java | 7 ++++++- 12 files changed, 86 insertions(+), 24 deletions(-) diff --git a/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java b/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java index 1ed03d84..0c887a8b 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java b/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java index 7fb600e4..b232ad47 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java @@ -7,9 +7,8 @@ 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 */ @@ -17,5 +16,9 @@ @Target({ElementType.TYPE}) @Repeatable(GhostMultiple.class) public @interface Ghost { + + /** + * The type and name of the ghost variable + */ public String value(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java index 8b42d74a..62778175 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java b/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java index 85aff527..5304bd5b 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java @@ -6,8 +6,8 @@ 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 */ @@ -15,7 +15,13 @@ @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 ""; } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java index 5274514a..a8bc5250 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java @@ -7,8 +7,8 @@ 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 */ @@ -16,5 +16,9 @@ @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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java index a4b2256e..d8596295 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java index aabea663..855e74fe 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java index 3af7267b..74914905 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java index 18a57fe3..ca7e2d07 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java @@ -7,10 +7,8 @@ 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 */ @@ -18,9 +16,19 @@ @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 ""; } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java index 0280fcbe..fe79f5f8 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java index 71549eca..5545a36a 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java @@ -7,9 +7,8 @@ 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 */ @@ -17,5 +16,9 @@ @Target({ElementType.TYPE}) @Repeatable(StateSets.class) public @interface StateSet { + + /** + * The array of states to be created + */ public String[] value(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java index ecd10fdf..9e3b8257 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java +++ b/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(); } From 160c6cc33fa1d295d67dd9756f4abe34b1736bd8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 11 Feb 2026 22:38:06 +0000 Subject: [PATCH 2/2] Improve Javadocs --- .../specification/ExternalRefinementsFor.java | 30 +++++++++-- .../java/liquidjava/specification/Ghost.java | 29 ++++++++-- .../specification/GhostMultiple.java | 9 +--- .../liquidjava/specification/Refinement.java | 42 ++++++++++++--- .../specification/RefinementAlias.java | 31 +++++++++-- .../RefinementAliasMultiple.java | 9 +--- .../specification/RefinementPredicate.java | 34 +++++++++--- .../RefinementPredicateMultiple.java | 9 +--- .../specification/StateRefinement.java | 53 +++++++++++++++---- .../StateRefinementMultiple.java | 9 +--- .../liquidjava/specification/StateSet.java | 27 ++++++++-- .../liquidjava/specification/StateSets.java | 10 +--- .../testBooleanGhost/BooleanGhostClass.java | 2 +- .../ArrayListRefinements.java | 2 +- 14 files changed, 216 insertions(+), 80 deletions(-) diff --git a/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java b/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java index 0c887a8b..3faef58e 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java +++ b/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. + *

+ * 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. + *

+ * Example: + * 

+ * {@code
+ * @ExternalRefinementsFor("java.lang.Math")
+ * public interface MathRefinements {
+ *     @Refinement("_ >= 0")
+ *     public double sqrt(double x);
+ * }
+ * }
+ *
* - * @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. + *

+ * Example: + * 

+     * {@code
+     * @ExternalRefinementsFor("java.lang.Math")
+     * }
+     *
*/ - public String value(); + String value(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java b/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java index b232ad47..195b5693 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java @@ -7,10 +7,22 @@ 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. + *

+ * 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. + *

+ * Example: + * 

+ * {@code
+ * @Ghost("int size")
+ * public class MyStack {
+ *     // ...
+ * }
+ * }
+ *
* - * @author catarina gamboa + * @author Catarina Gamboa */ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE}) @@ -18,7 +30,14 @@ public @interface Ghost { /** - * The type and name of the ghost variable + * The type and name of the ghost variable. + *

+ * Example: + * 

+     * {@code
+     * @Ghost("int size")
+     * }
+     *
*/ - public String value(); + String value(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java index 62778175..4aea5a73 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java b/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java index 5304bd5b..5ec2dec9 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java +++ b/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. + *

+ * Refinements are logical predicates that must hold for the annotated element. + *

+ * Example: + * 

+ * {@code
+ * @Refinement("x > 0")
+ * int x;
+ * 
+ * @Refinement("_ >= 0")
+ * public int getSize() {
+ *     // ...
+ * }
+ * }
+ *
* - * @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. + *

+ * Example: + * 

+     * {@code
+     * @Refinement("x > 0")
+     * }
+     *
*/ - 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). + *

+ * Example: + * 

+     * {@code
+     * @Refinement(value = "x > 0", msg = "x must be positive")
+     * }
+     *
*/ - public String msg() default ""; + String msg() default ""; } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java index a8bc5250..01253d56 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java @@ -7,10 +7,24 @@ 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. + *

+ * Refinement aliases can be used to define reusable refinement predicates with parameters. + * They help reduce duplication and improve readability of complex refinement specifications. + *

+ * Example: + * 

+ * {@code
+ * @RefinementAlias("Nat(int x) { x > 0 }")
+ * public class MyClass {
+ *     @Refinement("Nat(_)")
+ *     int value;
+ * }
+ * }
+ *
* - * @author catarina gamboa + * @see Refinement + * @author Catarina Gamboa */ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE}) @@ -18,7 +32,14 @@ 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. + *

+ * Example: + * 

+     * {@code
+     * @RefinementAlias("Nat(int x) { x > 0 }")
+     * }
+     *
*/ - public String value(); + String value(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java index d8596295..2f5e93e0 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java index 855e74fe..44d7f4df 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java @@ -7,10 +7,24 @@ 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. + *

+ * This annotation enables the declaration of ghosts and refinement aliases. + *

+ * Example: + * 

+ * {@code
+ * @RefinementPredicate("ghost int size")
+ * @RefinementPredicate("type Nat(int x) { x > 0 }")
+ * public void process() {
+ *     // ...
+ * }
+ * }
+ *
+ * + * @see Ghost + * @see RefinementAlias + * @author Catarina Gamboa */ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) @@ -18,7 +32,15 @@ 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. + *

+ * Example: + * 

+     * {@code
+     * @RefinementPredicate("ghost int size")
+     * @RefinementPredicate("type Nat(int x) { x > 0 }")
+     * }
+     *
*/ - public String value(); + String value(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java index 74914905..ca512fa8 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java index ca7e2d07..2d235891 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java @@ -7,10 +7,24 @@ 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. + *

+ * 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. + *

+ * Example: + * 

+ * {@code
+ * @StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")
+ * public void close() {
+ *     // ...
+ * }
+ * }
+ *
* - * @author catarina gamboa + * @see StateSet + * @author Catarina Gamboa */ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) @@ -18,17 +32,38 @@ 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) + *

+ * Example: + * 

+     * {@code
+     * @StateRefinement(from="open(this)")
+     * }
+     *
*/ - 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) + *

+ * Example: + * 

+     * {@code
+     * @StateRefinement(from="open(this)", to="closed(this)")
+     * }
+     *
*/ - 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) + *

+ * Example: + * 

+     * {@code
+     * @StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")
+     * }
+     *
*/ - public String msg() default ""; + String msg() default ""; } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java index fe79f5f8..c410a4db 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java +++ b/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(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java index 5545a36a..d1d0dbb3 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java @@ -7,10 +7,20 @@ import java.lang.annotation.Target; /** - * Annotation to create the disjoint states in which class objects can be - * e.g. @StateSet({"open", "reading", "closed"}) + * Annotation to create a set of disjoint states in which class objects can be. + *

+ * 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. + *

+ * Example: + * 

+ * {@code
+ * @StateSet({"open", "reading", "closed"}})
+ *
* - * @author catarina gamboa + * @see StateRefinement + * @author Catarina Gamboa */ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE}) @@ -18,7 +28,14 @@ public @interface StateSet { /** - * The array of states to be created + * The array of states to be created. + *

+ * Example: + * 

+     * {@code
+     * @StateSet({"open", "reading", "closed"})
+     * }
+     *
*/ - public String[] value(); + String[] value(); } diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java index 9e3b8257..817a0c91 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java @@ -6,17 +6,11 @@ import java.lang.annotation.Target; /** - * Annotation to allow the creation of multiple `@StateSet` annotations - * e.g. `@StateSets({@StateSet({"open", "reading", "closed"}), @StateSet({"on", "off"})})` - * - * @author catarina gamboa + * Annotation to allow the creation of multiple state sets. + * @author Catarina Gamboa */ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE}) public @interface StateSets { - - /** - * The array of `@StateSet` annotations to be created - */ StateSet[] value(); } diff --git a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java index 1c08c349..6ddcb077 100644 --- a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java +++ b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java @@ -3,7 +3,7 @@ import liquidjava.specification.Ghost; import liquidjava.specification.StateRefinement; -@Ghost("boolean opened") +@Ghost(value="boolean opened") @Ghost("boolean closed") public class BooleanGhostClass { diff --git a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/ArrayListRefinements.java index c1c9151a..20c36c46 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/ArrayListRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/ArrayListRefinements.java @@ -5,7 +5,7 @@ import liquidjava.specification.Refinement; import liquidjava.specification.StateRefinement; -@ExternalRefinementsFor("java.util.ArrayList") +@ExternalRefinementsFor(value="java.util.ArrayList") @Ghost("int size") public interface ArrayListRefinements {