Ghost boolean (#46)

Author: rodrigomilisse

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();
+	}
+}

liquidjava-example/src/main/java/testSuite/classes/vending_machine_correct/VendingMachine.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() {}
+}

liquidjava-verifier/.gitignore

@@ -1 +1,2 @@
 spooned
+.antlr

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -77,15 +77,15 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
         Predicate c = new Predicate();
         List<GhostFunction> sets = getDifferentSets(tc, klass); // ??
         for (GhostFunction sg : sets) {
-            if (sg.getReturnType().toString().equals("int")) {
-                Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s),
-                        Predicate.createLit("0", Utils.INT));
-                c = Predicate.createConjunction(c, p);
-            } else {
-                // TODO: Implement other stuff
-                throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in"
-                        + " AuxStateHandler defaultState");
-            }
+            String retType = sg.getReturnType().toString();
+            Predicate typePredicate = switch (retType) {
+            case "int" -> Predicate.createLit("0", Utils.INT);
+            case "boolean" -> Predicate.createLit("false", Utils.BOOLEAN);
+            case "double" -> Predicate.createLit("0.0", Utils.DOUBLE);
+            default -> throw new RuntimeException("Ghost not implemented for type " + retType);
+            };
+            Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), typePredicate);
+            c = Predicate.createConjunction(c, p);
         }
         ObjectState os = new ObjectState();
         os.setTo(c);