Update Tests

Author: rcosta358

liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.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/testBooleanGhost/BooleanGhostTest.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_correct/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_correct/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/boolean_ghost_error/SimpleStateMachine.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/boolean_ghost_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/scoreboard_error/Scoreboard.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();
+	}
+}

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

@@ -0,0 +1,14 @@
+package testSuite.classes.vending_machine_correct;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("double value")
+public class VendingMachine {
+
+    @StateRefinement(from = "value(this) >= 0.0", to = "value(this) == value(old(this)) + 0.1")
+    void insertTenCents() {}
+
+    @StateRefinement(from = "value(this) >= 0.3")
+    void buy() {}
+}