From 5cbf73d031d27414a6db1c28d50988d2fdba6cec Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 7 Apr 2026 14:29:03 +0100 Subject: [PATCH 1/2] Remove Keywords from Ghost & Alias Declarations --- liquidjava-example/src/main/java/testSuite/CorrectAlias.java | 2 +- .../src/main/java/testSuite/CorrectAliasMultiple.java | 4 ++-- .../src/main/java/testSuite/CorrectSearchValueIndexArray.java | 2 +- .../src/main/java/testSuite/ErrorAliasSimple.java | 2 +- .../src/main/java/testSuite/ErrorAliasTypeMismatch.java | 4 ++-- .../src/main/java/testSuite/ErrorGhostArgsTypes.java | 2 +- .../src/main/java/testSuite/ErrorGhostNumberArgs.java | 2 +- .../testSuite/ErrorImplementationSearchValueIntArray.java | 2 +- .../src/main/java/testSuite/ErrorSearchValueIntArray.java | 2 +- .../src/main/java/testSuite/classes/car_correct/Car.java | 2 +- .../classes/input_reader_correct/InputStreamReaderRefs.java | 2 +- liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 | 4 ++-- 12 files changed, 15 insertions(+), 15 deletions(-) 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..72b8dac09 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectSearchValueIndexArray.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectSearchValueIndexArray.java @@ -5,7 +5,7 @@ public class CorrectSearchValueIndexArray { - @RefinementPredicate("ghost int length(int[])") + @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/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..3eff9cbcf 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java @@ -4,7 +4,7 @@ import liquidjava.specification.RefinementPredicate; public class ErrorGhostArgsTypes { - @RefinementPredicate("ghost boolean open(int)") + @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 index c29f83df6..58cb9c426 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java @@ -5,7 +5,7 @@ public class ErrorGhostNumberArgs { - @RefinementPredicate("ghost boolean open(int)") + @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 index 9a26aeb59..f60abe9c1 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java @@ -5,7 +5,7 @@ public class ErrorImplementationSearchValueIntArray { - @RefinementPredicate("ghost int length(int[])") + @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 index 01d213a9c..4991bedd9 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray.java @@ -5,7 +5,7 @@ public class ErrorSearchValueIntArray { - @RefinementPredicate("ghost int length(int[])") + @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/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/input_reader_correct/InputStreamReaderRefs.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct/InputStreamReaderRefs.java index 61f285597..3bf047542 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 @@ -10,7 +10,7 @@ @ExternalRefinementsFor("java.io.InputStreamReader") public interface InputStreamReaderRefs { - @RefinementPredicate("boolean open(InputStreamReader i)") + @RefinementPredicate("boolean open(InputStreamReader)") @StateRefinement(to = "open(this)") public void InputStreamReader(InputStream in); 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)?; From e3d8bc1b5163321c227e757cf576b5bf88802c42 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 7 Apr 2026 14:47:52 +0100 Subject: [PATCH 2/2] Change RefinementPredicate Target From Methods to Types --- .../specification/RefinementPredicate.java | 20 +++++++++---------- .../RefinementPredicateMultiple.java | 2 +- .../warnings/NonExistentConstructor.java | 2 +- .../warnings/NonExistentMethod.java | 2 +- .../CorrectSearchValueIndexArray.java | 2 +- .../java/testSuite/ErrorGhostArgsTypes.java | 2 +- .../java/testSuite/ErrorGhostNumberArgs.java | 3 +-- ...rrorImplementationSearchValueIntArray.java | 2 +- .../testSuite/ErrorSearchValueIntArray.java | 2 +- .../WarningExtRefNonExistentMethod.java | 2 +- .../WarningExtRefWrongConstructor.java | 2 +- .../WarningExtRefWrongParameterType.java | 2 +- .../testSuite/WarningExtRefWrongRetType.java | 2 +- .../ArrayListRefinements.java | 2 +- .../classes/email_correct/Email.java | 2 +- .../testSuite/classes/email_error/Email.java | 2 +- .../InputStreamReaderRefs.java | 2 +- .../InputStreamReaderRefinements.java | 2 +- .../InputStreamReaderRefinements.java | 2 +- .../classes/order_gift_correct/Order.java | 2 +- .../ArrayListRefinements.java | 2 +- .../ArrayListRefinements.java | 2 +- .../main/java/testingInProgress/Email.java | 2 +- .../java/testingInProgress/OrderSimple.java | 2 +- .../StringBuilderRefinements.java | 2 +- .../ExternalRefinementTypeChecker.java | 2 +- .../refinement_checker/TypeChecker.java | 8 ++++---- 27 files changed, 39 insertions(+), 40 deletions(-) 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/CorrectSearchValueIndexArray.java b/liquidjava-example/src/main/java/testSuite/CorrectSearchValueIndexArray.java index 72b8dac09..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("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 index 3eff9cbcf..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("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 58cb9c426..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("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 f60abe9c1..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("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 4991bedd9..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("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/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 3bf047542..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)") @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/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 {