Refactor Refinement Predicate

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>
      */

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();
 }

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);
 

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();
 

liquidjava-example/src/main/java/testSuite/CorrectAlias.java

@@ -4,7 +4,7 @@
 import liquidjava.specification.RefinementAlias;
 
 @SuppressWarnings("unused")
-@RefinementAlias("type PtGrade(int x) { x >= 0 && x <= 20}")
+@RefinementAlias("PtGrade(int x) { x >= 0 && x <= 20}")
 public class CorrectAlias {
 
     public static void main(String[] args) {

liquidjava-example/src/main/java/testSuite/CorrectAliasMultiple.java

@@ -4,8 +4,8 @@
 import liquidjava.specification.RefinementAlias;
 
 @SuppressWarnings("unused")
-@RefinementAlias("type Positive(double x) { x > 0}")
-@RefinementAlias("type PtGrade(double x) { x >= 0 && x <= 20}")
+@RefinementAlias("Positive(double x) { x > 0}")
+@RefinementAlias("PtGrade(double x) { x >= 0 && x <= 20}")
 public class CorrectAliasMultiple {
 
     public static void main(String[] args) {

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("ghost 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) {

liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java

@@ -4,7 +4,7 @@
 import liquidjava.specification.RefinementAlias;
 
 @SuppressWarnings("unused")
-@RefinementAlias("type PtGrade(double x) { x >= 0 && x <= 20}")
+@RefinementAlias("PtGrade(double x) { x >= 0 && x <= 20}")
 public class ErrorAliasSimple {
 
     public static void main(String[] args) {

liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java

@@ -4,8 +4,8 @@
 import liquidjava.specification.RefinementAlias;
 
 @SuppressWarnings("unused")
-@RefinementAlias("type Positive(int x) { x > 0}")
-@RefinementAlias("type PtGrade(double x) { x >= 0 && x <= 20}")
+@RefinementAlias("Positive(int x) { x > 0}")
+@RefinementAlias("PtGrade(double x) { x >= 0 && x <= 20}")
 public class ErrorAliasTypeMismatch {
 
     public static void main(String[] args) {

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("ghost boolean open(int)")
     @Refinement("open(4.5) == true")
     public int one() {
         return 1; // Argument Mismatch Error

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("ghost boolean open(int)")
     @Refinement("open(1,2) == true")
     public int one() {
         return 1; // Argument Mismatch Error

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("ghost 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) {

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("ghost 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) {

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();
 

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);
 

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();
 

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();
 

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();
 

liquidjava-example/src/main/java/testSuite/classes/car_correct/Car.java

@@ -4,7 +4,7 @@
 import liquidjava.specification.RefinementAlias;
 
 @RefinementAlias("Positive(int x) { x > 0}")
-@RefinementAlias("type CarAcceptableYears(int x) { x > 1800 && x < 2050}")
+@RefinementAlias("CarAcceptableYears(int x) { x > 1800 && x < 2050}")
 @RefinementAlias("GreaterThan(int x, int y) {x > y}")
 public class Car {
 

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<>();

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<>();

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 i)")
     @StateRefinement(to = "open(this)")
     public void InputStreamReader(InputStream in);
 

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);
 

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);
 

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() {}
 

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();
 

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();
 

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<>();

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() {}
 

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();
 

liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4

@@ -67,10 +67,10 @@ literal:
 //----------------------- Declarations -----------------------
 
 alias:
-	'type'? ID_UPPER '(' argDeclID ')' '{' pred '}';
+	ID_UPPER '(' argDeclID ')' '{' pred '}';
 
 ghost:
-	'ghost'? type ID ('(' argDecl? ')')?;
+	type ID ('(' argDecl? ')')?;
 
 argDecl:
 	type ID? (',' argDecl)?;

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);
         }