Skip to content

Update README #56

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rcosta358 merged 1 commit into from
Sep 28, 2025
Merged

Update README #56

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
109 changes: 59 additions & 50 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 4 additions & 0 deletions liquidjava
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
#!/bin/bash
mvn exec:java -pl liquidjava-verifier \
-Dexec.mainClass="liquidjava.api.CommandLineLauncher" \
-Dexec.args="$*"