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.

Example:

@Refinement("a > 0")
int a = 3; // okay
a = -8; // type error!

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:

• LiquidJava Website
• VS Code Extension (Marketplace)
• VS Code Extension (Source Code)
• LiquidJava Examples
• LiquidJava External Libraries Examples

The easiest way to use LiquidJava is through its VS Code extension, which uses the LiquidJava verifier directly inside VS Code, with real-time error diagnostics and syntax highlighting for refinements.

For development, you may use the LiquidJava verifier from the command line.

Before setting up LiquidJava, ensure you have the following installed:

• Java 20+ - JDK for compiling and running Java programs
• Maven 3.6+ - For building and dependency management

Additionally, you'll need the following dependency, which includes the LiquidJava API annotations:

<dependency>
    <groupId>io.github.liquid-java</groupId>
    <artifactId>liquidjava-api</artifactId>
    <version>0.0.5</version>
</dependency>

repositories {
    mavenCentral()
}

dependencies {
    implementation 'io.github.liquid-java:liquidjava-api:0.0.5'
}

1. Clone the repository: git clone https://github.com/liquid-java/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

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.

mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project"

If you're on Linux/macOS, you can use the liquidjava script (from the repository root) to simplify the process. The script recompiles the verifier only when local sources or Maven files have changed.

The LiquidJava verifier can be run from the command line with the following options:

Test a correct case:

./liquidjava liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java

This should output: Correct! Passed Verification.

Test an error case:

./liquidjava liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java

This should output an error message describing the refinement violation.

Run mvn test to run all the tests in LiquidJava.

The starter test file is TestExamples.java, which runs the test suite under the testSuite directory in liquidjava-example.

The test suite considers test cases:

1. Files that start with Correct or Error (e.g., CorrectRecursion.java)
2. Directories that contain the word correct or error (e.g., arraylist_correct)

Therefore, the files and folders that do not follow this pattern are ignored.

For failing test cases, the expected error must be specified as follows:

1. In singular test files, the expected error (title) should be written in the first line of the file as a comment
2. In test directories, a .expected file should be included in that directory with the expected error (title)

• docs: Contains documents used for the design of the language. This folder includes a README 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