Merge branch 'main' into multiple_args

Author: rcosta358

.vscode/launch.json

@@ -0,0 +1,12 @@
+{
+  "configurations": [
+    {
+      "type": "java",
+      "name": "Run LiquidJava",
+      "request": "launch",
+      "mainClass": "liquidjava.api.CommandLineLauncher",
+      "projectName": "liquidjava-verifier",
+      "args": "liquidjava-example/src/main/java/test"
+    }
+  ]
+}

README.md

@@ -2,90 +2,99 @@
 
 ![LiquidJava Banner](docs/design/figs/banner.gif)
 
-## Welcome to LiquidJava
+## Welcome to LiquidJava!
 
-LiquidJava is an additional type checker for Java that based on liquid types and typestates.
+LiquidJava is an additional type checker for Java, based on **liquid types** and **typestates**, which provides additional safety guarantees to Java programs through **refinements** at compile time.
 
-Simple example:
+**Example:**
 
 ```java
 @Refinement("a > 0")
 int a = 3; // okay
 a = -8; // type error!
 ```
 
-This project has the LiquidJava verifier, the API and some examples for testing.
+This project contains the LiquidJava verifier and its API, as well as some examples for testing.
+
 You can find out more about LiquidJava in the following resources:
 
-* [Try it](https://github.com/CatarinaGamboa/liquidjava-examples) with Codespaces or locally following these steps
-* [Website](https://catarinagamboa.github.io/liquidjava.html)
-* [Examples of LiquidJava](https://github.com/CatarinaGamboa/liquidjava-examples)
-* [LiquidJava Specification of the Java Standard Library](https://github.com/CatarinaGamboa/liquid-java-external-libs)
-* [VSCode plugin for LiquidJava](https://github.com/CatarinaGamboa/vscode-liquidjava)
+* [Try it](https://github.com/CatarinaGamboa/liquidjava-examples) with GitHub Codespaces or locally
+* [VS Code extension for LiquidJava](https://github.com/CatarinaGamboa/vscode-liquidjava)
+* [LiquidJava website](https://catarinagamboa.github.io/liquidjava.html)
+* [LiquidJava specification examples for the Java standard library](https://github.com/CatarinaGamboa/liquid-java-external-libs)
 <!-- * [Formalization of LiquidJava](https://github.com/CatarinaGamboa/liquidjava-formalization) - not opensource yet -->
 
-# Setup the project
+## Getting Started
+
+### VS Code Extension
+
+The easiest way to use LiquidJava is through its [VS Code extension](https://github.com/CatarinaGamboa/vscode-liquidjava), which uses the LiquidJava verifier directly inside VS Code, with error diagnostics and syntax highlighting for refinements.
+
+### Command Line
+
+For development, you may use the LiquidJava verifier from the command line.
+
+#### Prerequisites
 
-## 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.
+- Java 20+ - JDK for compiling and running Java programs
+- Maven 3.6+ - For building and dependency management
 
-## Installation Steps
+#### Setup
 
-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`.
+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
+#### Run Verification
 
-To check your refinements using LiquidJava:
+To run LiquidJava, use the Maven command below, replacing `/path/to/your/project` with the path to the Java file or directory you want to verify.
 
-**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"
+mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project"
 ```
-   This should output: `Correct! Passed Verification`.
 
-**Test an error case**:
+If you're on Linux/macOS, you can use the `liquidjava` script (from the repository root) to simplify the process.
+
+**Test a correct case**:
 ```bash
-mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java"
+./liquidjava liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java
 ```
-   This should output an error message describing the refinement violation.
 
-## Run verification
+This should output: `Correct! Passed Verification`.
 
-### In a specific project
+**Test an error case**:
+```bash
+./liquidjava liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java
+```
 
-Run the file `liquidjava-verifier\api\CommandLineLaucher` with the path to the target project for verification.
-If there are no arguments given, the application verifies the project on the path `liquidjava-example\src\main\java`.
+This should output an error message describing the refinement violation.
 
-## Testing
+#### Testing
 
 Run `mvn test` to run all the tests in LiquidJava.
 
-The starter test file is `TestExamples.java` which uses the test suite under the `liquidjava-examples/testSuite`.
-
-Paths in the test suite are considered test cases if:
+The starter test file is `TestExamples.java`, which runs the test suite under the `testSuite` directory in `liquidjava-example`.
 
-1. File that start with `Correct` or `Error` (e.g, "CorrectRecursion.java")
-2. Package/Folder that contains the word `correct` or `error`.
+The test suite considers test cases:
+1. Files that start with `Correct` or `Error` (e.g., `CorrectRecursion.java`)
+2. Packages or folders that contain the word `correct` or `error` (e.g., `arraylist_correct`)
 
-Therefore, files/folders that do not pass this description are not verified.
+Therefore, the files and folders that do not follow this pattern are ignored.
 
-## Project structure
+## Project Structure
 
-* **docs**: documents used for the design of the language. The folder includes a readme to a full artifact used in the design process, here are some initial documents used to prepare the design of the refinements language at its evaluation
-* **liquidjava-api**: inlcudes the annotations that can be introduced in the Java programs to add the refinements
-* **liquidjava-examples**: includes a main folder with the current example that the verifier is testing; the test suite that is used in maven test is under the `testSuite` folder
-* **liquidjava-verifier**: has the project for verification of the classes
-  * *api*: classes that test the verifier. Includes the `CommandLineLauncher` that runs the verification on a given class or on the main folder of `liquidjava-examples` if no argument is given. This package includes the JUnit tests to verify if the examples in `liquidjava-example/tests` are correctly verified.
-  * *ast*: represents the abstract syntax tree of the refinement's language.
-  * *errors*: package for reporting the errors.
-  * *processor*: package that handles the type checking.
-  * *rj_language*: handles the processing of the strings with refinements.
-  * *smt*: package that handles the translation to the SMT solver and the processing of the results the SMT solver produces.
-  * *utils*: includes useful methods for all the previous packages.
-  * *test/java/liquidjava/api/tests* contains the `TestExamples` class used for running the test suite.
+* **docs**: Contains documents used for the design of the language. This folder includes a [README](./docs/design/README.md) with the link to the full artifact used in the design process. It also contains initial documents used to prepare the design of the refinements language during its evaluation
+* **liquidjava-api**: Includes the annotations that can be introduced in the Java programs to add the refinements
+* **liquidjava-example**: Includes some examples and the test suite used for testing the verifier
+* **liquidjava-verifier**: Includes the implementation of the verifier. Its main packages are:
+  * `api`: Includes the `CommandLineLauncher` that runs the verification on a given class or in the `currentlyTesting` directory if no argument is given
+  * `ast`: Represents the Abstract Syntax Tree (AST) of the Refinements Language (RJ)
+  * `errors`: Package for reporting the errors
+  * `processor`: Package that handles the type checking
+  * `rj_language`: Handles the parsing of the refinement strings to an AST
+  * `smt`: Package that handles the translation to the SMT solver and the processing of the results the SMT solver produces
+  * `utils`: Includes useful methods for all the previous packages
+  * `test/java/liquidjava/api/tests`: Contains the `TestExamples` class used for running the test suite

liquidjava

@@ -0,0 +1,4 @@
+#!/bin/bash
+mvn exec:java -pl liquidjava-verifier \
+  -Dexec.mainClass="liquidjava.api.CommandLineLauncher" \
+  -Dexec.args="$*"

liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Door.java

@@ -0,0 +1,11 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.StateSet;
+import liquidjava.specification.StateRefinement;
+
+@StateSet({"open", "closed"})
+public class Door {
+
+    @StateRefinement(to = "open(this)")
+    public Door() { }
+}

liquidjava-example/src/main/java/testSuite/classes/ambiguous_state_names_correct/Pipe.java

@@ -0,0 +1,11 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.StateSet;
+import liquidjava.specification.StateRefinement;
+
+@StateSet({"open", "closed"})
+public class Pipe {
+    
+    @StateRefinement(to = "open(this)")
+    public Pipe() { }
+}

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

@@ -0,0 +1,14 @@
+package testSuite.classes.ambiguous_state_names_correct;
+
+import liquidjava.specification.Refinement;
+
+public class SimpleTest {
+
+    public static void main(String[] args) {
+        Door d = new Door(); // contains 'open' and 'closed' states
+        Pipe p = new Pipe(); // unrelated type with the same state names
+        requiresOpen(d); // ok iff 'open' binds to Door.open otherwise it may bind to Pipe.open and fail
+    }
+
+    public static void requiresOpen(@Refinement("open(s)") Door s) { }
+}

liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM1.java

@@ -0,0 +1,15 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"uninitialized", "initialized"})
+public class SM1 {
+
+	@StateRefinement(to="uninitialized(this)")
+	public SM1() {}
+	
+
+	@StateRefinement(from="uninitialized(this)", to="initialized(this)")
+	public void initialize() {}
+}

liquidjava-example/src/main/java/testSuite/classes/conflicting_state_names_correct/SM2.java

@@ -0,0 +1,15 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"uninitialized", "initialized"})
+public class SM2 {
+
+	@StateRefinement(to="uninitialized(this)")
+	public SM2() {}
+	
+
+	@StateRefinement(from="uninitialized(this)", to="initialized(this)")
+	public void initialize() {}
+}

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

@@ -0,0 +1,11 @@
+package testSuite.classes.conflicting_state_names_correct;
+
+class SimpleTest {
+	public static void main(String[] args) {
+		// both classes contain the same state names
+		SM1 sm1 = new SM1();
+		SM2 sm2 = new SM2();
+		sm1.initialize();
+		sm2.initialize();
+	}
+}

liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java

@@ -181,8 +181,7 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter
         sb.append(element + "\n\n");
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
-        sb.append(sb.toString());
-
+        
         errorl.addError(s, sb.toString(), element.getPosition(), 1);
     }