Merge branch 'main' into improve-test-suite

Author: cheestree

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

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class CorrectEnumField {
+    enum Color {
+        Red, Green, Blue
+    }
+
+    @Refinement("color != Color.Blue")
+    Color color;
+
+    void setColor(@Refinement("c != Color.Blue") Color c) {
+        color = c;
+    }
+
+    public static void main(String[] args) {
+        CorrectEnumField cef = new CorrectEnumField();
+        cef.setColor(Color.Red);   // correct
+        cef.setColor(Color.Green); // correct
+    }
+}

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

@@ -0,0 +1,19 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class CorrectEnumParam {
+    enum Status {
+        Active, Inactive, Pending
+    }
+
+    Status process(@Refinement("status == Status.Inactive") Status status) {
+        return Status.Active;
+    }
+
+    public static void main(String[] args) {
+        CorrectEnumParam cep = new CorrectEnumParam();
+        cep.process(Status.Inactive); // correct
+    }
+}

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

@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+class CorrectEnumRefinement {
+    enum Lever {
+        Up, Down, Middle
+    }
+
+    public static void main(String[] args) {
+        @Refinement("_==Lever.Up || _==Lever.Down")
+        Lever lever = Lever.Up;
+        System.out.println(lever);
+    }
+}

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

@@ -0,0 +1,45 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@SuppressWarnings("unused")
+@StateSet({"photoMode", "videoMode", "noMode"})
+class CorrectEnumUsage {
+	enum Mode {
+		Photo, Video, Unknown
+	}
+
+	Mode mode;
+	@StateRefinement(to="noMode(this)")
+	public CorrectEnumUsage() {}
+
+	@StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)")
+	@StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)")
+	public void setMode(Mode mode) {
+		this.mode = mode;
+	}
+
+	@StateRefinement(from="photoMode(this)", to="noMode(this)")
+	@StateRefinement(from="videoMode(this)", to="noMode(this)")
+	public void resetMode() {
+		this.mode = null;
+	}
+	
+	@StateRefinement(from="photoMode(this)")
+	public void takePhoto() {}
+
+	@StateRefinement(from="videoMode(this)")
+	public void takeVideo() {}
+	
+	
+	public static void main(String[] args) {
+		// Correct
+		CorrectEnumUsage st = new CorrectEnumUsage();
+		st.setMode(Mode.Photo);  // noMode -> photoMode
+		st.takePhoto();
+		st.resetMode();          // photoMode -> noMode
+		st.setMode(Mode.Video);  // noMode -> videoMode
+		st.takeVideo();
+	}
+}

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

@@ -0,0 +1,22 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumFunctionRefinement {
+    enum Color { Red, Green, Blue }
+
+	Color c;
+
+	Color changeColor(@Refinement("newColor == Color.Red || newColor == Color.Green") Color newColor) {
+		c = newColor; // correct
+		return c;
+	}
+	
+	public static void main(String[] args) {
+		ErrorEnumFunctionRefinement e = new ErrorEnumFunctionRefinement();
+		e.changeColor(Color.Red); // correct
+		e.changeColor(Color.Blue); // error
+	}
+}

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

@@ -0,0 +1,19 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumNegation {
+    enum Status {
+        Active, Inactive, Pending
+    }
+
+    void process(@Refinement("status != Status.Inactive") Status status) {}
+
+    public static void main(String[] args) {
+        ErrorEnumNegation e = new ErrorEnumNegation();
+        e.process(Status.Active);   // correct
+        e.process(Status.Inactive); // error
+    }
+}

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

@@ -0,0 +1,16 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumNull {
+	enum Color {
+		Red, Green, Blue
+	}
+	
+	public static void main(String[] args) {
+		@Refinement("c == Color.Red || c == Color.Green")
+		Color c = null; // error
+	}
+}

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

@@ -0,0 +1,35 @@
+// State Refinement Error
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+
+@SuppressWarnings("unused")
+@StateSet({"photoMode", "videoMode", "noMode"})
+class ErrorEnumUsage {
+	enum Mode {
+		Photo, Video, Unknown
+	}
+
+	Mode mode;
+	@StateRefinement(to="noMode(this)")
+	public ErrorEnumUsage() {}
+
+	@StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)")
+	@StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)")
+	public void setMode(Mode mode) {
+		this.mode = mode;
+	}
+	
+	@StateRefinement(from="photoMode(this)")
+	public void takePhoto() {}
+	
+	
+	public static void main(String[] args) {
+		// Correct
+		ErrorEnumUsage st = new ErrorEnumUsage();
+		st.setMode(Mode.Video);
+		st.takePhoto(); //error
+	}
+}

liquidjava-verifier/pom.xml

@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.14</version>
+	<version>0.0.16</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>

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

@@ -38,12 +38,14 @@ literalExpression:
 	|	literal						#lit
 	| 	ID 							#var
 	|	functionCall				#invocation
+	|	enumerate					#enum
 	;
 
- functionCall:
+functionCall:
  		ghostCall
  	|	aliasCall
-	|	dotCall;
+	|	dotCall
+	;
 
 dotCall:
 		OBJECT_TYPE '(' args? ')'
@@ -55,6 +57,9 @@ ghostCall:
 aliasCall:
 	ID_UPPER '(' args? ')';
 
+enumerate: 
+	ENUM;
+
 args:	pred (',' pred)* ;
 
 
@@ -94,6 +99,7 @@ ARITHOP : '+'|'*'|'/'|'%';//|'-';
 
 BOOL    : 'true' | 'false';
 ID_UPPER: ([A-Z][a-zA-Z0-9]*);
+ENUM: [A-Z][a-zA-Z0-9_]* '.' [A-Z][a-zA-Z0-9_]*;
 OBJECT_TYPE:
 		  (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);
 ID     	: '#'*[a-zA-Z_][a-zA-Z0-9_#]*;