Counter

A simple refinement example for ensuring a counter never decrements below zero.

Diagnostic Explorer

Explore how you can use the diagnostic explorer to understand failures interactively.

Errors

Learn about the different verification errors LiquidJava can report and what each one means.

Getting Started

Set up your environment and run your first LiquidJava verification.

Real-Time Diagnostic Feedback

Find out about real-time diagnostic reporting directly in the editor.

@Refinement

Learn about how to use refinements to specify constraints on variables, fields, parameters, and return values.

Setup

Set up the dependency, verifier, and VS Code extension to start using LiquidJava.

Context Debugger

See how you can use the context debugger to debug failed refinements.

Annotations

Learn the different annotations in LiquidJava for writing specifications.

Overview

Learn what LiquidJava adds to Java.

Pagination

Plain refinements with aliases for page numbers, page sizes, and computed offsets.

@RefinementAlias

Learn how to reuse common refinement predicates with aliases to keep contracts shorter and easier to maintain.

Syntax Highlighting for Refinements

Learn about syntax highlighting for refinements in the VS Code extension.

Warnings

Learn about the different verification warnings LiquidJava can report and what each one means.

Autocomplete for Refinements

Explore context-aware auto-completion support for refinement predicates.

Custom Messages

Learn how to provide clearer diagnostic messages.

Diagnostics

Learn about the different types of errors and warnings, how to use custom error messages, and how to interpret refinement errors.

Media Player

A typestate protocol for a simple media player.

State Machine Visualizer

Find out about the state machine visualizer for classes with state refinements.

@StateRefinement

Learn how to model protocol-oriented object states and valid method transitions.

Email

A typestate protocol for an Email builder API.

@ExternalRefinementsFor

Learn how to refine external libraries that cannot be annotated directly.

Webview

Delve into the VS Code webview with interactive diagnostic explorer, context debugger, and state machine visualizer.

VS Code Extension

Use the LiquidJava VS Code extension for live diagnostics, syntax highlighting, and IDE feedback while editing Java code.

Understanding Refinement Errors

Learn how to read and interpret LiquidJava refinement errors.

Command-Line Interface

Run the LiquidJava verifier from the command line for local checks, debugging, and CI workflows.

@Ghost

Learn how to track logical state that helps express and verify richer object invariants.

Order

A typestate protocol for a simple order processing system.

Status Bar Indicator

Check out the indicator that shows the current state of LiquidJava.

Commands

Explore the commands provided by the extension for various interactions.

Downloader

A typestate protocol for a downloader object.

Examples

LiquidJava example usages with focused code snippets.

@RefinementPredicate

Learn how to declare custom ghost functions and how they relate to ghosts and states.

Connection

A typestate protocol with a value-dependent conditional transition.

Output Channel

Discover the output channel for LiquidJava logs.

Resources

Find LiquidJava papers, posters, and source repositories for deeper reading and experimentation.

ArrayList

An external refinement for ArrayList that prevents out-of-bounds access.