Merge branch 'main' into decouple-z3

Author: rcosta358

README.md

@@ -55,6 +55,8 @@ To run LiquidJava, use the Maven command below, replacing `/path/to/your/project
 ```bash
 mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project"
 ```
+*Warning: Any change to LiquidJava requires rebuilding the jar.*
+
 
 If you're on Linux/macOS, you can use the `liquidjava` script (from the repository root) to simplify the process.
 

liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java

@@ -0,0 +1,39 @@
+package testBooleanGhost;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("boolean opened")
+@Ghost("boolean closed")
+public class BooleanGhostClass {
+
+	boolean opened;
+	boolean closed;
+
+	@StateRefinement(from = "!opened(this) && !closed(this)", to = "opened(this) && !closed(this)")
+	void open() {
+		opened = true;
+	}
+
+	@StateRefinement(from = "opened(this) && !closed(this)")
+	void execute() {
+		// System.out.println("opened:" + open + "\nclosed::" + closed); // lança
+		// exceção
+
+		System.out.println("opened: ");
+		System.out.println(opened);
+		System.out.println("\nclosed: ");
+		System.out.println(closed);
+
+	}
+
+	@StateRefinement(from = "opened(this) && !closed(this)", to = "opened(this) && closed(this)")
+	void close() {
+		closed = true;
+	}
+
+	@StateRefinement(from = "opened(this) && closed(this)")
+	void terminate() {
+		System.out.println("Terminating\n");
+	}
+}

liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java

@@ -0,0 +1,12 @@
+package testBooleanGhost;
+
+public class BooleanGhostTest {
+	public static void main(String[] args) {
+		BooleanGhostClass bgc = new BooleanGhostClass();
+
+		bgc.open(); // ccomment out for error
+		bgc.execute();
+		bgc.close(); // comment out for error
+		bgc.terminate();
+	}
+}

liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleStateMachine.java

@@ -0,0 +1,17 @@
+package testSuite.classes.boolean_ghost_correct;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("boolean open")
+public class SimpleStateMachine {
+
+	@StateRefinement(from = "!open(this)", to = "open(this)")
+	void open() {}
+
+	@StateRefinement(from = "open(this)")
+	void execute() {}
+
+	@StateRefinement(from = "open(this)", to = "!open(this)")
+	void close() {}
+}

liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_correct/SimpleTest.java

@@ -0,0 +1,10 @@
+package testSuite.classes.boolean_ghost_correct;
+
+public class SimpleTest {
+	public static void main(String[] args) {
+		SimpleStateMachine ssm = new SimpleStateMachine();
+		ssm.open();
+		ssm.execute();
+		ssm.close();
+	}
+}

liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleStateMachine.java

@@ -0,0 +1,17 @@
+package testSuite.classes.boolean_ghost_error;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("boolean open")
+public class SimpleStateMachine {
+	
+	@StateRefinement(from = "!open(this)", to = "open(this)")
+	void open() {}
+
+	@StateRefinement(from = "open(this)")
+	void execute() {}
+
+	@StateRefinement(from = "open(this)", to = "!open(this)")
+	void close() {}
+}

liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/SimpleTest.java

@@ -0,0 +1,10 @@
+package testSuite.classes.boolean_ghost_error;
+
+public class SimpleTest {
+	public static void main(String[] args) {
+		SimpleStateMachine ssm = new SimpleStateMachine();
+		ssm.open();
+		ssm.close();
+		ssm.execute(); // error, not open
+	}
+}

liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/Scoreboard.java

@@ -0,0 +1,17 @@
+package testSuite.classes.scoreboard_error;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("double value")
+public class Scoreboard {
+
+    @StateRefinement(from = "value(this) < 1.0", to = "value(this) == value(old(this)) + 0.1")
+    public void inc() {}
+
+    @StateRefinement(from = "value(this) > 0.0", to = "value(this) == value(old(this)) - 0.1")
+    public void dec() {}
+
+    @StateRefinement(from = "value(this) > 0.0")
+    public void finish() {}
+}

liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/SimpleTest.java

@@ -0,0 +1,11 @@
+package testSuite.classes.scoreboard_error;
+
+public class SimpleTest {
+	public static void main(String[] args) {
+		Scoreboard sb = new Scoreboard();
+		sb.inc();
+		sb.dec();
+		sb.dec(); // error, underflow
+		sb.finish();
+	}
+}

liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/SimpleTest.java

@@ -0,0 +1,11 @@
+package testSuite.classes.vending_machine_correct;
+
+public class SimpleTest {
+	public static void main(String[] args) {
+		VendingMachine vm = new VendingMachine(); // 30 cents to buy
+		vm.insertTenCents();
+		vm.insertTenCents();
+		vm.insertTenCents();
+		vm.buy();
+	}
+}