Skip to content

Commit dd5083c

Browse files
rcosta358rcosta358
authored
Update Annotations Javadocs (#144)
1 parent 3fefa2f commit dd5083c

File tree

12 files changed

+246
-45
lines changed

12 files changed

+246
-45
lines changed

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

Lines changed: 26 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,18 +6,37 @@
66
import java.lang.annotation.Target;
77

88
/**
9-
* Annotation to create refinements for an external library. The annotation receives the path of the
10-
* library e.g. @ExternalRefinementsFor("java.lang.Math")
9+
* Annotation to refine a class or interface of an external library.
10+
* <p>
11+
* This annotation allows you to specify refinements and state transitions for classes from external libraries
12+
* that you cannot directly annotate. The refinements apply to all instances of the specified class.
13+
* <p>
14+
* <strong>Example:</strong>
15+
* <pre>
16+
* {@code
17+
* @ExternalRefinementsFor("java.lang.Math")
18+
* public interface MathRefinements {
19+
* @Refinement("_ >= 0")
20+
* public double sqrt(double x);
21+
* }
22+
* }
23+
* </pre>
1124
*
12-
* @author catarina gamboa
25+
* @author Catarina Gamboa
1326
*/
1427
@Retention(RetentionPolicy.RUNTIME)
1528
@Target({ElementType.TYPE})
1629
public @interface ExternalRefinementsFor {
30+
1731
/**
18-
* The prefix of the external method
19-
*
20-
* @return
32+
* The fully qualified name of the class or interface for which the refinements are being defined.
33+
* <p>
34+
* <strong>Example:</strong>
35+
* <pre>
36+
* {@code
37+
* @ExternalRefinementsFor("java.lang.Math")
38+
* }
39+
* </pre>
2140
*/
22-
public String value();
41+
String value();
2342
}

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

Lines changed: 27 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,15 +7,37 @@
77
import java.lang.annotation.Target;
88

99
/**
10-
* Annotation to create a ghost variable for a class. The annotation receives
11-
* the type and name of
12-
* the ghost within a string e.g. @Ghost("int size")
10+
* Annotation to create a ghost variable for a class or interface.
11+
* <p>
12+
* Ghost variables that only exist during the verification and can be used in refinements and state refinements.
13+
* They are not part of the actual implementation but help specify behavior and invariants.
14+
* <p>
15+
* <strong>Example:</strong>
16+
* <pre>
17+
* {@code
18+
* @Ghost("int size")
19+
* public class MyStack {
20+
* // ...
21+
* }
22+
* }
23+
* </pre>
1324
*
14-
* @author catarina gamboa
25+
* @author Catarina Gamboa
1526
*/
1627
@Retention(RetentionPolicy.RUNTIME)
1728
@Target({ElementType.TYPE})
1829
@Repeatable(GhostMultiple.class)
1930
public @interface Ghost {
20-
public String value();
31+
32+
/**
33+
* The type and name of the ghost variable.
34+
* <p>
35+
* <strong>Example:</strong>
36+
* <pre>
37+
* {@code
38+
* @Ghost("int size")
39+
* }
40+
* </pre>
41+
*/
42+
String value();
2143
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66
import java.lang.annotation.Target;
77

88
/**
9-
* Annotation to allow the creation of multiple @Ghost
9+
* Annotation to allow the creation of multiple ghost variables.
1010
*
11-
* @author catarina gamboa
11+
* @author Catarina Gamboa
1212
*/
1313
@Retention(RetentionPolicy.RUNTIME)
1414
@Target({ElementType.TYPE})

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

Lines changed: 38 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,49 @@
66
import java.lang.annotation.Target;
77

88
/**
9-
* Annotation to add a refinement to variables, class fields, method's parameters and method's
10-
* return value e.g. @Refinement("x > 0") int x;
9+
* Annotation to add a refinement to variables, class fields, method's parameters and method's return values.
10+
* <p>
11+
* Refinements are logical predicates that must hold for the annotated element.
12+
* <p>
13+
* <strong>Example:</strong>
14+
* <pre>
15+
* {@code
16+
* @Refinement("x > 0")
17+
* int x;
18+
*
19+
* @Refinement("_ > 0")
20+
* int increment(@Refinement("_ >= 0") int n) {
21+
* return n + 1;
22+
* }
23+
* </pre>
1124
*
12-
* @author catarina gamboa
25+
* @author Catarina Gamboa
1326
*/
1427
@Retention(RetentionPolicy.RUNTIME)
1528
@Target({ElementType.METHOD, ElementType.FIELD, ElementType.LOCAL_VARIABLE, ElementType.PARAMETER, ElementType.TYPE})
1629
public @interface Refinement {
1730

18-
public String value();
31+
/**
32+
* The refinement string that defines a logical predicate that must hold for the annotated element.
33+
* <p>
34+
* <strong>Example:</strong>
35+
* <pre>
36+
* {@code
37+
* @Refinement("x > 0")
38+
* }
39+
* </pre>
40+
*/
41+
String value();
1942

20-
public String msg() default "";
43+
/**
44+
* Custom error message to be shown when the refinement is violated (optional).
45+
* <p>
46+
* <strong>Example:</strong>
47+
* <pre>
48+
* {@code
49+
* @Refinement(value = "x > 0", msg = "x must be positive")
50+
* }
51+
* </pre>
52+
*/
53+
String msg() default "";
2154
}

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

Lines changed: 29 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,39 @@
77
import java.lang.annotation.Target;
88

99
/**
10-
* Annotation to create a ghost variable for a class. The annotation receives the type and name of
11-
* the ghost within a string e.g. @RefinementAlias("Nat(int x) {x > 0}")
10+
* Annotation to create a refinement alias to be reused in refinements.
11+
* <p>
12+
* Refinement aliases can be used to define reusable refinement predicates with parameters.
13+
* They help reduce duplication and improve readability of complex refinement specifications.
14+
* <p>
15+
* <strong>Example:</strong>
16+
* <pre>
17+
* {@code
18+
* @RefinementAlias("Nat(int x) { x > 0 }")
19+
* public class MyClass {
20+
* @Refinement("Nat(_)")
21+
* int value;
22+
* }
23+
* }
24+
* </pre>
1225
*
13-
* @author catarina gamboa
26+
* @see Refinement
27+
* @author Catarina Gamboa
1428
*/
1529
@Retention(RetentionPolicy.RUNTIME)
1630
@Target({ElementType.TYPE})
1731
@Repeatable(RefinementAliasMultiple.class)
1832
public @interface RefinementAlias {
19-
public String value();
33+
34+
/**
35+
* The refinement alias string, which includes the name of the alias, its parameters and the refinement itself.
36+
* <p>
37+
* <strong>Example:</strong>
38+
* <pre>
39+
* {@code
40+
* @RefinementAlias("Nat(int x) { x > 0 }")
41+
* }
42+
* </pre>
43+
*/
44+
String value();
2045
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66
import java.lang.annotation.Target;
77

88
/**
9-
* Annotation to create a multiple Alias in a class
9+
* Annotation to create multiple refinement aliases.
1010
*
11-
* @author catarina gamboa
11+
* @author Catarina Gamboa
1212
*/
1313
@Retention(RetentionPolicy.RUNTIME)
1414
@Target({ElementType.TYPE})

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

Lines changed: 33 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,41 @@
66
import java.lang.annotation.RetentionPolicy;
77
import java.lang.annotation.Target;
88

9+
/**
10+
* Annotation that allows the creation of ghost variables or refinement aliases within method or constructor scope.
11+
* <p>
12+
* This annotation enables the declaration of ghosts and refinement aliases.
13+
* <p>
14+
* <strong>Example:</strong>
15+
* <pre>
16+
* {@code
17+
* @RefinementPredicate("ghost int size")
18+
* @RefinementPredicate("type Nat(int x) { x > 0 }")
19+
* public void process() {
20+
* // ...
21+
* }
22+
* }
23+
* </pre>
24+
*
25+
* @see Ghost
26+
* @see RefinementAlias
27+
* @author Catarina Gamboa
28+
*/
929
@Retention(RetentionPolicy.RUNTIME)
1030
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
1131
@Repeatable(RefinementPredicateMultiple.class)
1232
public @interface RefinementPredicate {
13-
public String value();
33+
34+
/**
35+
* The refinement predicate string, which can define a ghost variable or a refinement alias.
36+
* <p>
37+
* <strong>Example:</strong>
38+
* <pre>
39+
* {@code
40+
* @RefinementPredicate("ghost int size")
41+
* @RefinementPredicate("type Nat(int x) { x > 0 }")
42+
* }
43+
* </pre>
44+
*/
45+
String value();
1446
}

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,11 @@
55
import java.lang.annotation.RetentionPolicy;
66
import java.lang.annotation.Target;
77

8+
/**
9+
* Annotation to allow the creation of multiple refinement predicates.
10+
*
11+
* @author Catarina Gamboa
12+
*/
813
@Retention(RetentionPolicy.RUNTIME)
914
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
1015
public @interface RefinementPredicateMultiple {

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

Lines changed: 51 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,20 +7,63 @@
77
import java.lang.annotation.Target;
88

99
/**
10-
* Annotation to create state transitions in a method. The annotation has three arguments: from : the
11-
* state in which the object needs to be for the method to be invoked correctly to : the state in
12-
* which the object will be after the execution of the method msg : optional custom error message to display when refinement is violated
13-
* e.g. @StateRefinement(from="open(this)", to="closed(this)")
10+
* Annotation to create state transitions in a method using states defined in state sets.
11+
* <p>
12+
* This annotation specifies the required precondition state and the resulting
13+
* postcondition state when a method or constructor is invoked.
14+
* Constructors can only specify the postcondition state since they create a new object.
15+
* <p>
16+
* <strong>Example:</strong>
17+
* <pre>
18+
* {@code
19+
* @StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")
20+
* public void close() {
21+
* // ...
22+
* }
23+
* }
24+
* </pre>
1425
*
15-
* @author catarina gamboa
26+
* @see StateSet
27+
* @author Catarina Gamboa
1628
*/
1729
@Retention(RetentionPolicy.RUNTIME)
1830
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
1931
@Repeatable(StateRefinementMultiple.class)
2032
public @interface StateRefinement {
21-
public String from() default "";
2233

23-
public String to() default "";
34+
/**
35+
* The logical pre-condition that defines the state in which the object needs to be before calling the method (optional)
36+
* <p>
37+
* <strong>Example:</strong>
38+
* <pre>
39+
* {@code
40+
* @StateRefinement(from="open(this)")
41+
* }
42+
* </pre>
43+
*/
44+
String from() default "";
2445

25-
public String msg() default "";
46+
/**
47+
* The logical post-condition that defines the state in which the object will be after calling the method (optional)
48+
* <p>
49+
* <strong>Example:</strong>
50+
* <pre>
51+
* {@code
52+
* @StateRefinement(from="open(this)", to="closed(this)")
53+
* }
54+
* </pre>
55+
*/
56+
String to() default "";
57+
58+
/**
59+
* Custom error message to be shown when the {@code from} pre-condition is violated (optional)
60+
* <p>
61+
* <strong>Example:</strong>
62+
* <pre>
63+
* {@code
64+
* @StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")
65+
* }
66+
* </pre>
67+
*/
68+
String msg() default "";
2669
}

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

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,9 @@
66
import java.lang.annotation.Target;
77

88
/**
9-
* Interface to allow multiple state refinements in a method. A method can have a state refinement
10-
* for each set of different source and destination states
9+
* Annotation to allow the creation of multiple state transitions.
1110
*
12-
* @author catarina gamboa
11+
* @author Catarina Gamboa
1312
*/
1413
@Retention(RetentionPolicy.RUNTIME)
1514
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})

0 commit comments

Comments
 (0)