Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Updated tests to fit with main changes
  • Loading branch information
cheestree committed Mar 30, 2026
commit 2754337162cbea3aeb3ff519573220e1f698027c
Original file line number Diff line number Diff line change
@@ -1,22 +1,23 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

@SuppressWarnings("unused")
class ErrorEnumFunctionRefinement {
enum Color { Red, Green, Blue }
enum Color {
Red, Green, Blue
}

Color c;

Color changeColor(@Refinement("newColor == Color.Red || newColor == Color.Green") Color newColor) {
c = newColor; // correct
c = newColor;
return c;
}

public static void main(String[] args) {
ErrorEnumFunctionRefinement e = new ErrorEnumFunctionRefinement();
e.changeColor(Color.Red); // correct
e.changeColor(Color.Blue); // error
e.changeColor(Color.Red);
e.changeColor(Color.Blue); // Refinement Error
}
}
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;
Expand All @@ -13,7 +12,7 @@ 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
e.process(Status.Active);
e.process(Status.Inactive); // Refinement Error
}
}
5 changes: 2 additions & 3 deletions liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;
Expand All @@ -8,9 +7,9 @@ class ErrorEnumNull {
enum Color {
Red, Green, Blue
}

public static void main(String[] args) {
@Refinement("c == Color.Red || c == Color.Green")
Color c = null; // error
Color c = null; // Refinement Error
}
}
Original file line number Diff line number Diff line change
@@ -1,10 +1,8 @@
// State Refinement Error
package testSuite;

import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;


@SuppressWarnings("unused")
@StateSet({"photoMode", "videoMode", "noMode"})
class ErrorEnumUsage {
Expand All @@ -21,7 +19,7 @@ public ErrorEnumUsage() {}
public void setMode(Mode mode) {
this.mode = mode;
}

@StateRefinement(from="photoMode(this)")
public void takePhoto() {}

Expand All @@ -30,6 +28,6 @@ public static void main(String[] args) {
// Correct
ErrorEnumUsage st = new ErrorEnumUsage();
st.setMode(Mode.Video);
st.takePhoto(); //error
st.takePhoto(); // State Refinement Error
}
}
Loading