Remove Keywords from Ghost & Alias Declarations

rcosta358 · rcosta358 · commit 5cbf73d031d2 · 2026-04-07T14:29:03.000+01:00
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)?;
