Skip to content

CLAUDE.md

Latest commit

 

History

History
77 lines (57 loc) · 4.54 KB

CLAUDE.md

File metadata and controls

77 lines (57 loc) · 4.54 KB
Raw

CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

Project Overview

LiquidJava is an additional type checker for Java that adds liquid types (refinements) and typestates on top of standard Java. Users annotate Java code with @Refinement, @StateRefinement, @StateSet etc. (from liquidjava-api); the verifier parses the program with Spoon, translates refinement predicates to SMT, and discharges verification conditions with Z3.

Requires Java 20+ and Maven 3.6+ (the parent POM declares 1.8 source/target, but the verifier module overrides to 20).

Module Layout

This is a Maven multi-module build (pom.xml is the umbrella):

  • liquidjava-api — published annotations (@Refinement, @RefinementAlias, @StateRefinement, @StateSet, ghost functions). Stable artifact users depend on.
  • liquidjava-verifier — the actual checker (Spoon processor + RJ AST + SMT translator). Published as io.github.liquid-java:liquidjava-verifier.
  • liquidjava-example — sample programs and the test suite under src/main/java/testSuite/. The verifier's tests scan this directory.

Verifier package map (liquidjava-verifier/src/main/java/liquidjava/):

  • api/ — entrypoints; CommandLineLauncher is the CLI main.
  • processor/ — Spoon processors. RefinementProcessor orchestrates; refinement_checker/ contains RefinementTypeChecker, MethodsFirstChecker, ExternalRefinementTypeChecker, plus general_checkers/ and object_checkers/ for typestate.
  • ast/ — AST of the Refinements Language (RJ).
  • rj_language/ — parser from refinement strings to RJ AST.
  • smt/ — Z3 translation (TranslatorToZ3, ExpressionToZ3Visitor, SMTEvaluator, Counterexample).
  • errors/, utils/, diagnostics/.

Commands

Build / install everything:

mvn clean install

Run the test suite (verifier module, runs whole testSuite/ dir):

mvn test

Run a single test method (JUnit 4/5 mix — both work via Surefire):

mvn -pl liquidjava-verifier -Dtest=TestExamples test
mvn -pl liquidjava-verifier -Dtest=TestExamples#testMultiplePaths test

Verify a specific file/directory from CLI (uses the liquidjava script in repo root, macOS/Linux):

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

Equivalent raw form:

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

Code formatting runs automatically in the validate phase via formatter-maven-plugin (configured for Java 20 in liquidjava-verifier/pom.xml); no separate lint command.

Test Suite Conventions

Tests are discovered by TestExamples#testPath (parameterized) under liquidjava-example/src/main/java/testSuite/:

  • Single-file cases: filename starts with Correct… or Error….
  • Directory cases: directory name contains the substring correct or error.
  • Anything else is ignored (so helper sources can live alongside).
  • Expected error for a failing case:
    • Single file: write the expected error title in a comment on the first line of the file.
    • Directory: place a .expected file in that directory containing the expected error title.

When adding new test cases, place them under liquidjava-example/src/main/java/testSuite/ following the naming rules above — that is the only way they get picked up.

Architecture Notes That Span Files

  • Two-pass typechecking. MethodsFirstChecker collects method signatures and refinement contracts before RefinementTypeChecker walks bodies, so forward references and recursion resolve. Edits to one usually need a matching change in the other.
  • Refinement string → AST → Z3. A @Refinement("a > 0") string flows: rj_language parser → ast nodes → smt/TranslatorToZ3 / ExpressionToZ3Visitor. New predicate forms generally require touching all three.
  • External refinements. ExternalRefinementTypeChecker plus *Refinements.java companion files specify contracts for third-party APIs without modifying their sources. The co-specifying-liquidjava skill covers this workflow.
  • Typestate lives in processor/refinement_checker/object_checkers/ and uses @StateRefinement / @StateSet from the API. Ghost-state predicates flow through the same SMT pipeline as value refinements.
  • Z3 dependency. The verifier shells out to Z3 via JNI bindings; failures often surface as SMTResult errors or counterexamples, not Java exceptions.