Project developed at Logo




content-photo

Extending Java with
Liquid Types

Extend your Java code with Refinement Types and catch bugs earlier!
LiquidJava implements an additional type system with Refinement Types on top of Java. It allows developers to express better restrictions on the code and discover more bugs before executing the program.







Learn more about LiquidJava!

GitHub organization Verifier, API, examples, external libs — all in one place. Documentation Annotation reference and language guide. Tutorial Hands-on walkthrough — learn LiquidJava by example. Research paper Usability-Oriented Design of Liquid Types for Java — ICSE 2023.
Get started

Refine your Java in three steps

The LiquidJava plugin runs inside Visual Studio Code and gives you inline diagnostics as you type — no separate verifier window to babysit.

Install for VS Code Get on Open VSX
  1. 1
    Set up your toolchain

    You'll need the basics installed first.

  2. 2
    Install the plugin

    One click from the Marketplace, or search LiquidJava inside VS Code's extensions panel.

  3. 3
    Add the API to your project

    Drop the LiquidJava API dependency into your build, sprinkle @Refinement annotations, and watch the diagnostics light up.

    Maven / Gradle setup → Tutorial guide →

Reference

Predicates

Refinement Types extend the language with predicates over basic types. @Refinement("x > 0") int x; declares an int refined by x > 0. Predicates live in quantifier-free linear integer arithmetic.

LiquidJava Examples

Find examples of LiquidJava in different parts of code.

Variables

Examples of refinements in variables and class fields

Methods

Examples of methods with refinements in their parameters and return value.

Classes

Examples of object type state modelling using State Sets and Ghost attributes
Variables

Refinements in Variables

Add a @Refinement wherever you already have a basic type — local variables, fields, or anywhere else.

Variable
Positive

The variable has a value greater than zero.

@Refinement("positive > 0")
int positive;
positive = 50;   // Correct
positive = -1;   // Error
Variable
Percentage

Lower and upper bounds set on a variable. The _ wildcard refers to the variable being refined.

@Refinement("_ >= 0 && _ <= 100")
int percentage;
percentage = 50;        // Correct
percentage = 10 + 99;   // Error
Class fields · alias
RGB fields

Class fields can be refined like any local variable. The RGB alias keeps each channel between 0 and 255.

@RefinementAlias("RGB(int x) { x >= 0 && x <= 255 }")
class MyColor {
  @Refinement("RGB(r)") int r;
  @Refinement("RGB(_)") int g;
  @Refinement("RGB(_)") int b;
}
Methods

Refinements in Methods

Both parameters and return values can be refined. Parameter refinements constrain how the method may be called; the return refinement constrains what the body may return.

Method · return
Absolute

Refine the return type with an annotation above the method. The _ wildcard refers to the return value.

@Refinement("_ >= 0 && _ >= n")
public static int absolute(int n) {
  if (0 <= n)  return n;
  else         return 0 - n;
}
Method · parameters
Add Bonus — Grade

Refine method parameters. Both must satisfy the Percentage alias, and bonus can refer to grade (later parameters can mention earlier ones, never the reverse).

@RefinementAlias("Percentage(int x) { x >= 0 && x <= 100 }")
public class Grade {

  @Refinement("Percentage(_)")
  public static int addBonus(
      @Refinement("Percentage(_)") int grade,
      @Refinement("Percentage(_) && bonus < grade") int bonus) {
    if ((bonus + grade) > 100) return 100;
    else                       return grade + bonus;
  }
}
Classes

Refinements in Classes

LiquidJava models object lifecycles with two primitives: @StateSet for named states and @Ghost for auxiliary integer/boolean properties. Methods declare allowed transitions with @StateRefinement(from = …, to = …); use old(this) inside to to refer to the pre-call state. Browse real JDK protocols below.