Change RefinementPredicate Target From Methods to Types

rcosta358 · rcosta358 · commit e3d8bc1b5163 · 2026-04-07T14:47:52.000+01:00
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java
@@ -7,17 +7,18 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation that allows the creation of ghost variables or refinement aliases within method or constructor scope.
+ * Annotation that allows the creation of custom ghost functions within classes or interfaces.
  * <p>
- * This annotation enables the declaration of ghosts and refinement aliases.
+ * This annotation enables the declaration of custom ghost functions.
  * <p>
  * <strong>Example:</strong>
  * <pre>
  * {@code
- * @RefinementPredicate("ghost int size")
- * @RefinementPredicate("type Nat(int x) { x > 0 }")
- * public void process() {
- *     // ...
+ * @RefinementPredicate("int totalPrice(Order o)")
+ * public class Order {
+ *     @StateRefinement(to = "totalPrice(this) == 0")
+ *     public Order() {
+ *     }
  * }
  * }
  * </pre>
@@ -27,18 +28,17 @@
  * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
-@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+@Target({ElementType.TYPE})
 @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 defines a ghost function declaration.
      * <p>
      * <strong>Example:</strong>
      * <pre>
      * {@code
-     * @RefinementPredicate("ghost int size")
-     * @RefinementPredicate("type Nat(int x) { x > 0 }")
+     * @RefinementPredicate("int totalPrice(Order o)")
      * }
      * </pre>
      */
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java
@@ -11,7 +11,7 @@
  * @author Catarina Gamboa
  */
 @Retention(RetentionPolicy.RUNTIME)
-@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+@Target({ElementType.TYPE})
 public @interface RefinementPredicateMultiple {
     RefinementPredicate[] value();
 }
diff --git a/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.StateRefinement;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface NonExistentConstructor<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @StateRefinement(to = "size(this) == 0")
     public void ArrayList(String wrongParameter);
 
diff --git a/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.StateRefinement;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface NonExistentMethod<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @StateRefinement(to = "size(this) == 0")
     public void ArrayList();
 
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectSearchValueIndexArray.java b/liquidjava-example/src/main/java/testSuite/CorrectSearchValueIndexArray.java
@@ -3,9 +3,9 @@
 import liquidjava.specification.Refinement;
 import liquidjava.specification.RefinementPredicate;
 
+@RefinementPredicate("int length(int[])")
 public class CorrectSearchValueIndexArray {
 
-    @RefinementPredicate("int length(int[])")
     @Refinement("(_ >= -1) && (_ < length(l))")
     public static int getIndexWithValue(
             @Refinement("length(l) > 0") int[] l, @Refinement("i >= 0 && i < length(l)") int i, int val) {
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java
@@ -3,8 +3,8 @@
 import liquidjava.specification.Refinement;
 import liquidjava.specification.RefinementPredicate;
 
+@RefinementPredicate("boolean open(int)")
 public class ErrorGhostArgsTypes {
-    @RefinementPredicate("boolean open(int)")
     @Refinement("open(4.5) == true")
     public int one() {
         return 1; // Argument Mismatch Error
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java
@@ -3,9 +3,8 @@
 import liquidjava.specification.Refinement;
 import liquidjava.specification.RefinementPredicate;
 
+@RefinementPredicate("boolean open(int)")
 public class ErrorGhostNumberArgs {
-
-    @RefinementPredicate("boolean open(int)")
     @Refinement("open(1,2) == true")
     public int one() {
         return 1; // Argument Mismatch Error
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java
@@ -3,9 +3,9 @@
 import liquidjava.specification.Refinement;
 import liquidjava.specification.RefinementPredicate;
 
+@RefinementPredicate("int length(int[])")
 public class ErrorImplementationSearchValueIntArray {
 
-    @RefinementPredicate("int length(int[])")
     @Refinement("(_ >= -1) && (_ < length(l))")
     public static int getIndexWithValue(
             @Refinement("length(l) > 0") int[] l, @Refinement("i >= 0 && i < length(l)") int i, int val) {
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java
@@ -3,9 +3,9 @@
 import liquidjava.specification.Refinement;
 import liquidjava.specification.RefinementPredicate;
 
+@RefinementPredicate("int length(int[])")
 public class ErrorSearchValueIntArray {
 
-    @RefinementPredicate("int length(int[])")
     @Refinement("(_ >= -1) && (_ < length(l))")
     public static int getIndexWithValue(
             @Refinement("length(l) > 0") int[] l, @Refinement("i >= 0 && i < length(l)") int i, int val) {
diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.StateRefinement;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface WarningExtRefNonExistentMethod<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @StateRefinement(to = "size(this) == 0")
     public void ArrayList();
 
diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.StateRefinement;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface WarningExtRefWrongConstructor<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @StateRefinement(to = "size(this) == 0")
     public void ArrayList(String wrongParameter);
 
diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.StateRefinement;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface WarningExtRefWrongParameterType<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @StateRefinement(to = "size(this) == 0")
     public void ArrayList();
 
diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.StateRefinement;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface WarningExtRefWrongRetType<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @StateRefinement(to = "size(this) == 0")
     public void ArrayList();
 
diff --git a/liquidjava-example/src/main/java/testSuite/classes/arraylist_correct/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/arraylist_correct/ArrayListRefinements.java
@@ -3,9 +3,9 @@
 import liquidjava.specification.*;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface ArrayListRefinements<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @StateRefinement(to = "size(this) == 0")
     public void ArrayList();
 
diff --git a/liquidjava-example/src/main/java/testSuite/classes/email_correct/Email.java b/liquidjava-example/src/main/java/testSuite/classes/email_correct/Email.java
@@ -14,13 +14,13 @@
 @RefinementAlias("SenderSet  (Email e) { state(e) == 2}")
 @RefinementAlias("ReceiverSet(Email e) { state(e) == 3}")
 @RefinementAlias("BodySet    (Email e) { state(e) == 4}")
+@RefinementPredicate("int state(Email e)")
 public class Email {
     private String sender;
     private List<String> receiver;
     private String subject;
     private String body;
 
-    @RefinementPredicate("int state(Email e)")
     @StateRefinement(to = "EmptyEmail(this)")
     public Email() {
         receiver = new ArrayList<>();
diff --git a/liquidjava-example/src/main/java/testSuite/classes/email_error/Email.java b/liquidjava-example/src/main/java/testSuite/classes/email_error/Email.java
@@ -10,13 +10,13 @@
 // add sender -> add multiple receivers -> add subject <optional> -> add body -> build()
 // @RefinementAlias("EmptyEmail(Email e) { state(e) == 1}")
 @SuppressWarnings("unused")
+@RefinementPredicate("int state(Email e)")
 public class Email {
     private String sender;
     private List<String> receiver;
     private String subject;
     private String body;
 
-    @RefinementPredicate("int state(Email e)")
     @StateRefinement(to = "state(this) == 1")
     public Email() {
         receiver = new ArrayList<>();
diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct/InputStreamReaderRefs.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct/InputStreamReaderRefs.java
@@ -8,9 +8,9 @@
 
 // https://docs.oracle.com/javase/7/docs/api/java/io/InputStreamReader.html
 @ExternalRefinementsFor("java.io.InputStreamReader")
+@RefinementPredicate("boolean open(InputStreamReader)")
 public interface InputStreamReaderRefs {
 
-    @RefinementPredicate("boolean open(InputStreamReader)")
     @StateRefinement(to = "open(this)")
     public void InputStreamReader(InputStream in);
 
diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/InputStreamReaderRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/InputStreamReaderRefinements.java
@@ -7,8 +7,8 @@
 
 // https://docs.oracle.com/javase/7/docs/api/java/io/InputStreamReader.html
 @ExternalRefinementsFor("java.io.InputStreamReader")
+@RefinementPredicate("boolean open(InputStreamReader i)")
 public interface InputStreamReaderRefinements {
-    @RefinementPredicate("boolean open(InputStreamReader i)")
     @StateRefinement(to = "open(this)")
     public void InputStreamReader(InputStream in);
 
diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/InputStreamReaderRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/InputStreamReaderRefinements.java
@@ -7,8 +7,8 @@
 
 // https://docs.oracle.com/javase/7/docs/api/java/io/InputStreamReader.html
 @ExternalRefinementsFor("java.io.InputStreamReader")
+@RefinementPredicate("boolean open(InputStreamReader i)")
 public interface InputStreamReaderRefinements {
-    @RefinementPredicate("boolean open(InputStreamReader i)")
     @StateRefinement(to = "open(this)")
     public void InputStreamReader(InputStream in);
 
diff --git a/liquidjava-example/src/main/java/testSuite/classes/order_gift_correct/Order.java b/liquidjava-example/src/main/java/testSuite/classes/order_gift_correct/Order.java
@@ -6,9 +6,9 @@
 import liquidjava.specification.StateSet;
 
 @StateSet({"empty", "addingItems", "checkout", "closed"})
+@RefinementPredicate("int totalPrice(Order o)")
 public class Order {
 
-    @RefinementPredicate("int totalPrice(Order o)")
     @StateRefinement(to = "(totalPrice(this) == 0) && empty(this)")
     public Order() {}
 
diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/ArrayListRefinements.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.StateRefinement;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface ArrayListRefinements<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @StateRefinement(to = "size(this) == 0")
     public void ArrayList();
 
diff --git a/liquidjava-example/src/main/java/testingInProgress/ArrayListRefinements.java b/liquidjava-example/src/main/java/testingInProgress/ArrayListRefinements.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.RefinementPredicate;
 
 @ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList l)")
 public interface ArrayListRefinements<E> {
 
-    @RefinementPredicate("int size(ArrayList l)")
     @Refinement("size(this) == 0")
     public void ArrayList();
 
diff --git a/liquidjava-example/src/main/java/testingInProgress/Email.java b/liquidjava-example/src/main/java/testingInProgress/Email.java
@@ -9,13 +9,13 @@
 // Suppose there is only one acceptable order to construct the email
 // add sender -> add multiple receivers -> add subject <optional> -> add body -> build()
 @SuppressWarnings("unused")
+@RefinementPredicate("int state(Email e)")
 public class Email {
     private String sender;
     private List<String> receiver;
     private String subject;
     private String body;
 
-    @RefinementPredicate("int state(Email e)")
     @StateRefinement(to = "state(this) == 1")
     public Email() {
         receiver = new ArrayList<>();
diff --git a/liquidjava-example/src/main/java/testingInProgress/OrderSimple.java b/liquidjava-example/src/main/java/testingInProgress/OrderSimple.java
@@ -5,9 +5,9 @@
 import liquidjava.specification.StateSet;
 
 @StateSet({"empty", "addingItems", "checkout", "closed"})
+@RefinementPredicate("int countItems(OrderSimple o)")
 public class OrderSimple {
 
-    @RefinementPredicate("int countItems(OrderSimple o)")
     @StateRefinement(to = "(countItems(this) == 0) && empty(this)")
     public OrderSimple() {}
 
diff --git a/liquidjava-example/src/main/java/testingInProgress/StringBuilderRefinements.java b/liquidjava-example/src/main/java/testingInProgress/StringBuilderRefinements.java
@@ -3,8 +3,8 @@
 import liquidjava.specification.RefinementPredicate;
 import liquidjava.specification.StateRefinement;
 
+@RefinementPredicate("int lengthS(StringBuilder s)")
 public interface StringBuilderRefinements {
-    @RefinementPredicate("int lengthS(StringBuilder s)")
     @StateRefinement(to = "lengthS() == 0")
     public void StringBuilder();
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
@@ -95,7 +95,7 @@ public <R> void visitCtMethod(CtMethod<R> method) {
 
     protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
         GhostDTO f = getGhostDeclaration(value, position);
-        if (element.getParent() instanceof CtInterface<?>) {
+        if (element instanceof CtInterface<?> || element.getParent() instanceof CtInterface<?>) {
             GhostFunction gh = new GhostFunction(f, factory, prefix);
             context.addGhostFunction(gh);
         }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -29,6 +29,7 @@
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtInterface;
+import spoon.reflect.declaration.CtType;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
 import spoon.reflect.visitor.CtScanner;
@@ -233,10 +234,9 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
 
     protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
         GhostDTO f = getGhostDeclaration(value, position);
-        if (element.getParent()instanceof CtClass<?> klass) {
-            GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName());
-            context.addGhostFunction(gh);
-        }
+        CtType<?> type = element instanceof CtType<?> t ? t : element.getParent()instanceof CtType<?> t ? t : null;
+        if (type != null)
+            context.addGhostFunction(new GhostFunction(f, factory, type.getQualifiedName()));
     }
 
     protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError {

Original file line number	Diff line number	Diff line change
`@@ -11,7 +11,7 @@`
`11`	`11`	`* @author Catarina Gamboa`
`12`	`12`	`*/`
`13`	`13`	`@Retention(RetentionPolicy.RUNTIME)`
`14`		`-@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})`
	`14`	`+@Target({ElementType.TYPE})`
`15`	`15`	`public @interface RefinementPredicateMultiple {`
`16`	`16`	`RefinementPredicate[] value();`
`17`	`17`	`}`