diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java
index 44d7f4df6..525c6ca12 100644
--- 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.
*
- * This annotation enables the declaration of ghosts and refinement aliases.
+ * This annotation enables the declaration of custom ghost functions.
*
* Example:
*
* {@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() {
+ * }
* }
* }
*
@@ -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.
*
* Example:
*
* {@code
- * @RefinementPredicate("ghost int size")
- * @RefinementPredicate("type Nat(int x) { x > 0 }")
+ * @RefinementPredicate("int totalPrice(Order o)")
* }
*
*/
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java
index ca512fa80..8c7b3e9e5 100644
--- 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
index eae37e3c2..2dc0a7d61 100644
--- 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 {
- @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
index 9d3d16e6e..5db17ce83 100644
--- 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 {
- @RefinementPredicate("int size(ArrayList l)")
@StateRefinement(to = "size(this) == 0")
public void ArrayList();
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectAlias.java b/liquidjava-example/src/main/java/testSuite/CorrectAlias.java
index b71289cc2..f97dd8063 100644
--- a/liquidjava-example/src/main/java/testSuite/CorrectAlias.java
+++ b/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) {
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectAliasMultiple.java b/liquidjava-example/src/main/java/testSuite/CorrectAliasMultiple.java
index 0cd838073..7aa1e4a28 100644
--- a/liquidjava-example/src/main/java/testSuite/CorrectAliasMultiple.java
+++ b/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) {
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectSearchValueIndexArray.java b/liquidjava-example/src/main/java/testSuite/CorrectSearchValueIndexArray.java
index c724d3ab3..8b876cb3d 100644
--- 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("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) {
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java
index 8caa03c45..ea4c110cd 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java
+++ b/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) {
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java
index 0618ae83a..037000bbc 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java
+++ b/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) {
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java
index d193ad7bd..d9a519674 100644
--- 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("ghost 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
index c29f83df6..2fd812d8d 100644
--- 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("ghost 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
index 9a26aeb59..877105773 100644
--- 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("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) {
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java
index 01d213a9c..3e0415f89 100644
--- 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("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) {
diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java
index b98e48db1..08d81de91 100644
--- 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 {
- @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
index a81ee0ed7..576a70e9e 100644
--- 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 {
- @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
index c847d9e73..988c465f4 100644
--- 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 {
- @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
index bbba0b9a1..97477b2ae 100644
--- 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 {
- @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
index 4dc910011..f13e42455 100644
--- 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 {
- @RefinementPredicate("int size(ArrayList l)")
@StateRefinement(to = "size(this) == 0")
public void ArrayList();
diff --git a/liquidjava-example/src/main/java/testSuite/classes/car_correct/Car.java b/liquidjava-example/src/main/java/testSuite/classes/car_correct/Car.java
index b059dfe7d..08112a808 100644
--- a/liquidjava-example/src/main/java/testSuite/classes/car_correct/Car.java
+++ b/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 {
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
index b989be804..8542b7e98 100644
--- 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 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
index 99ebd50e9..f845b8e6c 100644
--- 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 -> 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 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
index 61f285597..59ad0152f 100644
--- 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 i)")
@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
index fcfdb8df2..ba382b286 100644
--- 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
index 428531bb8..dda965cd9 100644
--- 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
index e554614a0..a8de9a1ef 100644
--- 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
index 493490f52..811925780 100644
--- 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 {
- @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
index a7b020441..799b44aaf 100644
--- 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 {
- @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
index 63236cd22..425ab872b 100644
--- 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 -> add body -> build()
@SuppressWarnings("unused")
+@RefinementPredicate("int state(Email e)")
public class Email {
private String sender;
private List 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
index f0eb70d40..a67aed04f 100644
--- 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
index d9d33d83c..018fd93cb 100644
--- 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/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
index d6f7f45f7..0486eab2b 100644
--- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
+++ b/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)?;
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
index 6e5f0f0dd..aa9370bda 100644
--- 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 void visitCtMethod(CtMethod 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
index 4cbbe5bf8..99070343a 100644
--- 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 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 {