+ * 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 prefix of the external method
- *
- * @return
+ * 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 7fb600e4..195b5693 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java
+++ b/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.
+ * + * 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})
@Repeatable(GhostMultiple.class)
public @interface Ghost {
- public String value();
+
+ /**
+ * The type and name of the ghost variable.
+ * + * Example: + *
+ * {@code
+ * @Ghost("int size")
+ * }
+ *
+ */
+ 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..4aea5a73 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java
+++ b/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})
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java b/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java
index 85aff527..5ec2dec9 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java
+++ b/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.
+ * + * 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 {
- public String value();
+ /**
+ * The refinement string that defines a logical predicate that must hold for the annotated element.
+ * + * Example: + *
+ * {@code
+ * @Refinement("x > 0")
+ * }
+ *
+ */
+ String value();
- public String msg() default "";
+ /**
+ * Custom error message to be shown when the refinement is violated (optional).
+ * + * Example: + *
+ * {@code
+ * @Refinement(value = "x > 0", msg = "x must be positive")
+ * }
+ *
+ */
+ 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..01253d56 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java
+++ b/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.
+ * + * 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})
@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.
+ * + * Example: + *
+ * {@code
+ * @RefinementAlias("Nat(int x) { x > 0 }")
+ * }
+ *
+ */
+ 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..2f5e93e0 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java
+++ b/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})
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java
index aabea663..44d7f4df 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java
+++ b/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.
+ * + * 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})
@Repeatable(RefinementPredicateMultiple.class)
public @interface RefinementPredicate {
- public String value();
+
+ /**
+ * 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 }")
+ * }
+ *
+ */
+ 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..ca512fa8 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java
+++ b/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 {
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java
index 18a57fe3..2d235891 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java
+++ b/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.
+ * + * 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})
@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)
+ * + * Example: + *
+ * {@code
+ * @StateRefinement(from="open(this)")
+ * }
+ *
+ */
+ 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)
+ * + * Example: + *
+ * {@code
+ * @StateRefinement(from="open(this)", to="closed(this)")
+ * }
+ *
+ */
+ String to() default "";
+
+ /**
+ * 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")
+ * }
+ *
+ */
+ 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..c410a4db 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java
+++ b/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})
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java
index 71549eca..d1d0dbb3 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java
+++ b/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.
+ * + * 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})
@Repeatable(StateSets.class)
public @interface StateSet {
- public String[] value();
+
+ /**
+ * The array of states to be created.
+ * + * Example: + *
+ * {@code
+ * @StateSet({"open", "reading", "closed"})
+ * }
+ *
+ */
+ 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..817a0c91 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java
@@ -6,9 +6,8 @@
import java.lang.annotation.Target;
/**
- * Interface to allow multiple StateSets in a class.
- *
- * @author catarina gamboa
+ * Annotation to allow the creation of multiple state sets.
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE})
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