Ghost boolean

.gitignore

@@ -10,6 +10,7 @@ spooned
 .springBeans
 .sts4-cache
 
+.idea
 
 # Created by https://www.gitignore.io/api/git,java,maven,eclipse,windows
 

README.md

@@ -24,12 +24,36 @@ You can find out more about LiquidJava in the following resources:
 * [VSCode plugin for LiquidJava](https://github.com/CatarinaGamboa/vscode-liquidjava)
 <!-- * [Formalization of LiquidJava](https://github.com/CatarinaGamboa/liquidjava-formalization) - not opensource yet -->
 
-## Setup the project
+# Setup the project
 
-1. Clone the repository;
-2. Run `setup.sh`, some dependencies include using `Java 20` or newer and using `Maven`.
-3. Open the project in your favorite IDE (we have used Eclipse and VSCode)
-4. Use the `pom.xml` in the root directory (which your IDE may have renamed to`liquidjava-umbrella`) to compile and run the tests.
+## Prerequisites
+Before setting up LiquidJava, ensure you have the following installed:
+
+- Java 20 or newer - The project is configured to use Java 20;
+- Maven 3.6+ - For building and dependency management.
+
+## Installation Steps
+
+1. Clone the repository: `git clone https://github.com/CatarinaGamboa/liquidjava.git`;
+2. Build the project `mvn clean install`;
+3. Run tests to verify installation: `mvn test`;
+4. If importing into an IDE, import the project as a Maven project using the root `pom.xml`.
+
+## Verify Installation
+
+To check your refinements using LiquidJava:
+
+**Run verification on examples**:
+```bash
+mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java"
+```
+   This should output: `Correct! Passed Verification`.
+
+**Test an error case**:
+```bash
+mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java"
+```
+   This should output an error message describing the refinement violation.
 
 ## Run verification
 

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-verifier/pom.xml

@@ -17,6 +17,7 @@
 	<packaging>jar</packaging>
 
 	<build>
+		<finalName>${jar.finalName}</finalName>
 		<plugins>
 			<plugin>
 				<groupId>net.revelc.code.formatter</groupId>
@@ -110,6 +111,8 @@
 		<!-- plugin versions -->
 		<pVersion.compiler>3.8.0</pVersion.compiler>
 		<pVersion.surefire>3.1.2</pVersion.surefire>
+		<!-- name of the generated plugin -->
+		<jar.finalName>${project.artifactId}-${project.version}</jar.finalName>
 	</properties>
 
 	<repositories>

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

@@ -83,9 +83,13 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
                 Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
                         Predicate.createLit("0", Utils.INT));
                 c = Predicate.createConjunction(c, p);
+            } else if (sg.getReturnType().toString().equals("boolean")) {
+                Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
+                        Predicate.createLit("false", Utils.BOOLEAN));
+                c = Predicate.createConjunction(c, p);
             } else {
                 // TODO: Implement other stuff
-                throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in"
+                throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in"
                         + " AuxStateHandler defaultState");
             }
         }