From 29888b62399cbe8ac2404aba3e43bb89659dbc3b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 6 Oct 2026 20:12:48 +0100 Subject: [PATCH] Update CLAUDE.md to match current test conventions and layout - Test discovery: any .java file outside a leaf dir, and every leaf dir; names are only a convention - Expectations use // Expect: Error / Warning comments - Package map: ast under rj_language, errors/warnings under diagnostics - Z3 bundled via z3-turnkey Java bindings; drop missing skill reference - Mention ./mvnw, script recompile behaviour, and CLI options Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --- CLAUDE.md | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index ec5b7aa2f..b663122c1 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -19,10 +19,10 @@ This is a Maven multi-module build (`pom.xml` is the umbrella): 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. +- `rj_language/` — the Refinements Language (RJ): `parsing/` (refinement strings → AST), `ast/`, `opt/` (expression simplification), `visitors/`. - `smt/` — Z3 translation (`TranslatorToZ3`, `ExpressionToZ3Visitor`, `SMTEvaluator`, `Counterexample`). -- `errors/`, `utils/`, `diagnostics/`. +- `diagnostics/` — error and warning reporting (`errors/`, `warnings/`). +- `utils/` — shared utilities and constants. ## Commands @@ -31,7 +31,7 @@ Build / install everything: mvn clean install ``` -Run the test suite (verifier module, runs whole `testSuite/` dir): +Run the test suite (verifier module, runs whole `testSuite/` dir); `./mvnw` works in place of `mvn`: ```bash mvn test ``` @@ -42,7 +42,7 @@ 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): +Verify a specific file/directory from CLI (uses the `liquidjava` script in repo root, macOS/Linux; it recompiles the verifier only when local sources or Maven files changed): ```bash ./liquidjava liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java ``` @@ -52,6 +52,7 @@ mvn exec:java -pl liquidjava-verifier \ -Dexec.mainClass="liquidjava.api.CommandLineLauncher" \ -Dexec.args="/path/to/file_or_dir" ``` +CLI options: one or more paths, `-h`/`--help`, `-v`/`--version`, `-d`/`--debug` (debug logging, skips expression simplification), `-lsp`/`--language-server`. 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. @@ -59,17 +60,17 @@ Code formatting runs automatically in the `validate` phase via `formatter-maven- 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 errors for a failing case are declared with inline `// <Error Title>` comments on **the line where each error should be reported** (regex `//\s*(.*?\bError\b)`, case-insensitive — see `TestUtils#getExpectedErrorsFromFile`). Both the title and the line number must match, and the count of comments must equal the count of reported errors. Directory cases work the same way: the scanner walks every file in the directory; there are no `.expected` files. +- Every `.java` file outside a leaf directory is a single-file test case. +- Every leaf directory (no subdirectories) is a single test case covering all its files. +- File and directory names do not matter (the `Correct…`/`Error…`/`…_correct`/`…_error` names are only a convention). +- Expected diagnostics are declared with inline `// Expect: <Title> Error` or `// Expect: Warning` comments on **the line where each diagnostic should be reported** (regex `//\s*Expect:\s*(.*?\b(Error|Warning)\b)`, case-insensitive — see `TestUtils#getExpectedDiagnosticsFromFile`). For errors both the title and the line must match; for warnings only the line. The number of expectations must equal the number of reported diagnostics, so a test with no expectations must produce none. Directory cases collect expectations from every file in the directory; there are no `.expected` files. -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. +When adding new test cases, place them under `liquidjava-example/src/main/java/testSuite/` — 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. +- **External refinements.** `ExternalRefinementTypeChecker` plus `*Refinements.java` companion files specify contracts for third-party APIs without modifying their sources. - **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. +- **Z3 dependency.** The verifier calls Z3 in-process through the Java bindings bundled by `z3-turnkey` (no separate Z3 install); failures often surface as `SMTResult` errors or counterexamples, not Java exceptions.