Agent Skills
› NeverSight/learn-skills.dev
› openjml
openjml
GitHub用于为Java程序编写JML形式化规格说明，并利用OpenJML工具进行静态验证(ESC)和运行时断言检查(RAC)。涵盖规格编写、验证执行、结果解读及失败调试全流程。
Trigger Scenarios
编写JML规格说明
使用OpenJML验证Java代码
调试OpenJML验证失败
审查JML规格正确性
Install
npx skills add NeverSight/learn-skills.dev --skill openjml -g -y
SKILL.md
Frontmatter
{
"name": "openjml",
"description": "Write JML (Java Modeling Language) specifications for Java programs and verify them using OpenJML. Covers the full workflow: writing specs, running static verification (ESC) and runtime assertion checking (RAC), interpreting verification results, and debugging failures."
}
JML Specification & OpenJML Verification
You are an expert at writing JML (Java Modeling Language) formal specifications for Java code and verifying them with OpenJML. Follow these instructions precisely when the user asks you to write, review, or debug JML specifications.
1. When To Use This Skill
Use this skill when the user asks you to:
- Write JML specifications (preconditions, postconditions, invariants, loop specs) for Java code
- Verify Java code with OpenJML (
--escor--rac) - Debug or fix OpenJML verification failures
- Review existing JML specs for correctness or completeness
- Explain JML syntax or semantics
Do NOT use this skill for non-Java languages or for testing frameworks (JUnit, etc.) unless the user explicitly wants JML-based verification alongside tests.
2. What Is JML
JML is a behavioral interface specification language for Java. Specifications are written as
specially-formatted Java comments (//@ for single-line, /*@ ... @*/ for multi-line) and
describe what methods must do, not how they do it. OpenJML is the tool that checks whether
Java code satisfies its JML specifications, using either:
- ESC (Extended Static Checking): Proves correctness at compile time via SMT solvers. No test inputs needed. This is the primary mode.
- RAC (Runtime Assertion Checking): Compiles specs into runtime checks, evaluated during execution. Useful when ESC times out or for integration testing.
3. JML Syntax Essentials
Comment Markers
//@ single-line JML annotation
/*@ multi-line
@ JML annotation
@*/
Method-Level Clauses
| Clause | Meaning |
|---|---|
requires P; |
Precondition: caller must establish P before calling |
ensures Q; |
Postcondition: method must establish Q on normal return |
assignable x, y; |
Frame condition: only x and y may be modified (aliases: assigns, modifies, writes) |
signals (E e) R; |
If exception E is thrown, R holds |
signals_only E1, E2; |
Only these checked exceptions may be thrown |
also |
Separates multiple specification cases |
normal_behavior |
Spec case that implies signals (Exception e) false; |
exceptional_behavior |
Spec case that implies ensures false; |
Class-Level Clauses
| Clause | Meaning |
|---|---|
invariant P; |
Must hold at entry and exit of every public method |
constraint P; |
History constraint: relates pre- and post-state |
initially P; |
Must hold after construction |
Loop Specifications
Place these immediately before the loop statement:
| Clause | Meaning |
|---|---|
maintaining P; (or loop_invariant) |
Invariant preserved by each iteration |
loop_writes x; (or loop_modifies, loop_assignable) |
Variables modified by loop body |
decreases E; |
Integer expression that decreases each iteration and is non-negative; proves termination |
Key Spec Expressions
| Expression | Meaning |
|---|---|
\result |
Return value of the method |
\old(expr) |
Value of expr at method entry |
\forall T x; range; body |
Universal quantification |
\exists T x; range; body |
Existential quantification |
\nothing |
Empty set (for assignable) |
\everything |
All memory (for assignable) |
P ==> Q |
Implication |
P <==> Q |
Bi-implication (if and only if) |
\count |
Loop iteration counter (inside maintaining) |
a[i..j] |
Array range (in quantified expressions, use explicit index) |
Chained Relationals
JML supports chained comparisons. Prefer them for clarity:
//@ requires 0 <= i && i < a.length;
// Better written as:
//@ requires 0 <= i < a.length;
Visibility and Purity
pure: Method has no side effects; can be used in specs. Impliesassignable \nothing;.spec_pure: Likepurebut verification only; no runtime check. Minimum required to use a method in a JML expression.strictly_pure: No side effects and does not read mutable state.no_state: Reads no state at all (only depends on parameters).nullable: Annotation on a parameter, return, or field to allow null. JML defaults everything to non-null.nullable_by_default: Class-level modifier to flip the default.
4. Specification Writing Process
Follow this exact sequence when writing JML specs for a method. Do not skip steps.
Step 1: Identify Purpose and Contract Type
- Is this a query (returns a value, no side effects)? Use
pureand focus onensures. - Is this a command (modifies state)? Focus on
assignable+ensures. - Can it throw exceptions? Plan
signals/signals_onlyclauses.
Step 2: Annotate Nullness
- JML defaults to
non_nullfor all reference types. - If any parameter, return, or field legitimately can be null, annotate it
/*@ nullable @*/. - If most things in the class are nullable, use
/*@ nullable_by_default @*/on the class.
Step 3: Write Preconditions (requires)
- State what must be true for the method to execute correctly.
- Order clauses so earlier ones establish well-definedness for later ones:
//@ requires a != null; // enables safe dereference //@ requires 0 <= i < a.length; // depends on a != null - Multiple
requiresclauses are conjoined (AND).
Step 4: Write Frame Conditions (assignable)
- List every field and array element that the method may modify.
- Use exactly ONE
assignableclause per spec case. Multipleassignableclauses compute their intersection, not union -- this is a critical gotcha. - If the method is pure, write
assignable \nothing;. - If you are unsure, start with
assignable \everything;and narrow it down. - For array elements:
assignable a[*];orassignable a[i..j];.
Step 5: Write Postconditions (ensures)
- Describe the return value with
\result. - Describe state changes using
\old(expr)to reference pre-state values. - Multiple
ensuresclauses are conjoined (AND). - Make postconditions strong enough for callers to reason about the result (see Section 9).
Step 6: Specify Exceptional Behavior
- Use
signals (ExceptionType e) condition;to describe when/why exceptions are thrown. - Use
signals_only ExceptionType;to restrict which exceptions may escape. - For methods that never throw:
signals (Exception e) false;or usenormal_behavior.
Step 7: Write Loop Specifications (if applicable)
Every loop MUST have all three parts:
maintaining: The loop invariant. Must include:- Range of the loop variable including the exit value (e.g.,
0 <= i <= a.length, NOT< a.length) - The inductive property being established
- Range of the loop variable including the exit value (e.g.,
loop_writes: Every variable or array element modified in the loop bodydecreases: An integer expression that strictly decreases each iteration
Step 8: Verify and Iterate
- Run
openjml --esc FileName.java - If verification fails, read the failure name and line number
- Consult Section 7 (failure remediation table) and Section 8 (common pitfalls)
- Fix the spec or code, then re-verify
- Repeat until exit code 0
5. Spec Templates
Use these fill-in templates as starting points. Replace {...} placeholders.
Pure Query Method
/*@ public normal_behavior
@ requires {precondition};
@ ensures \result == {expression relating params/fields to return value};
@*/
public /*@ pure @*/ {ReturnType} {methodName}({params}) {
...
}
State-Modifying Method
/*@ public normal_behavior
@ requires {precondition};
@ assignable {field1}, {field2};
@ ensures {field1} == {new value} && {field2} == \old({field2}) + {delta};
@*/
public void {methodName}({params}) {
...
}
Method with Normal + Exceptional Behavior
/*@ public normal_behavior
@ requires {normal precondition};
@ assignable {fields};
@ ensures {postcondition};
@ also
@ public exceptional_behavior
@ requires {exceptional precondition};
@ assignable \nothing;
@ signals_only {ExceptionType};
@*/
public {ReturnType} {methodName}({params}) throws {ExceptionType} {
...
}
Loop with Full Spec
//@ maintaining 0 <= i <= a.length;
//@ maintaining {inductive property over a[0..i)};
//@ loop_writes i, {other modified vars};
//@ decreases a.length - i;
for (int i = 0; i < a.length; i++) {
...
}
Class Invariant
public class {ClassName} {
private int {field};
//@ invariant {field} >= 0;
//@ invariant {other property};
...
}
6. Running OpenJML
Extended Static Checking (Primary)
openjml --esc FileName.java
- Exit code 0: All specifications verified.
- Exit code 6: One or more verification failures. Read output for failure names and locations.
- Other exit codes: Compilation errors, parse errors, or tool issues.
Useful ESC Flags
| Flag | Purpose |
|---|---|
--esc |
Run static verification |
--esc-max-warnings=N |
Limit number of warnings reported (default: all) |
--timeout=N |
Per-method timeout in seconds (default: varies) |
--method={name} |
Verify only the named method |
--prover=z3 |
Select SMT solver (z3 is default) |
--show |
Show the logical assertions being checked |
--trace |
Show a counterexample trace on failure |
--progress |
Show progress during verification |
--sourcepath=dir |
Add source path for dependent files |
--specspath=dir |
Add path to spec files (.jml) |
--classpath=path |
Set classpath for dependencies |
Runtime Assertion Checking
# Compile with RAC instrumentation:
openjml --rac FileName.java
# Run the instrumented class:
openjml --rac-run ClassName
RAC is useful when:
- ESC times out on complex methods
- You want to test specs against concrete inputs
- You want specs enforced during integration testing
Verifying Multiple Files
openjml --esc src/*.java
openjml --esc --sourcepath=src src/Main.java
Workflow Tip
Always verify incrementally: write specs for one method, verify, fix, then move to the next. Do not spec an entire class and then verify -- failures cascade and become hard to diagnose.
7. Interpreting & Fixing Verification Failures
When OpenJML reports a failure, the output contains a failure name and source location. Use this table to diagnose and fix the issue.
| Failure Name | Meaning | Likely Cause | Fix |
|---|---|---|---|
Postcondition |
ensures clause not satisfied at method exit |
Postcondition too strong, or implementation does not establish it | Weaken the postcondition, or fix the implementation. Check that all code paths satisfy it. |
Precondition |
Caller does not establish requires of a called method |
Missing precondition on the calling method, or calling without checking | Add requires to the caller that implies the callee's precondition. |
UndefinedCalledMethodPrecondition |
A method called in a spec expression has an unsatisfied precondition | Spec references a method whose own requires is not met |
Ensure the spec context guarantees the called method's preconditions. |
Assignable |
Method modifies something not listed in assignable |
Missing field/array in assignable, or called method has assignable \everything |
Add the modified location to assignable. Check called methods' frame conditions. |
PossiblyNullDeReference |
Potential null dereference | JML's non-null default is violated, or missing null check | Add requires x != null; or annotate the reference nullable and add a null guard. |
UndefinedNullDeReference |
Null dereference inside a spec expression | Spec expression dereferences something possibly null | Reorder requires so non-null is established first, or add explicit null check in spec. |
LoopInvariantBeforeLoop |
Loop invariant does not hold on loop entry | Invariant is wrong at initial values | Check that the invariant holds for the initial value of the loop variable. |
LoopInvariant |
Loop invariant not preserved by loop body | Body breaks the invariant, or invariant is too weak | Strengthen the invariant to account for body's modifications, or fix the body. |
LoopDecreases |
decreases expression does not strictly decrease |
Wrong variant expression, or loop modifies it unexpectedly | Fix the decreases expression to reflect the actual loop progress. |
InvariantEntrance |
Class invariant does not hold at method entry | Object was constructed/modified without establishing invariant | Check constructors and all methods that modify invariant-related fields. |
InvariantExit |
Class invariant does not hold at method exit | Method breaks the invariant | Ensure method re-establishes all class invariants before returning. |
ExceptionList |
Method throws an exception not in signals_only |
Uncovered exception type | Add the exception to signals_only, or add a signals clause for it. |
ArithmeticOperationRange |
Arithmetic overflow/underflow | Integer computation may overflow | Add preconditions bounding inputs, or cast to long before computing. |
ArrayIndex |
Array index out of bounds | Index not proven within [0, length) |
Add requires or maintaining that bounds the index. |
NegativeArraySize |
Array created with negative size | Size expression may be negative | Add requires size >= 0; or equivalent. |
Assert |
An explicit //@ assert P; failed |
The assertion is not provable at that point | Strengthen preceding specs or add intermediate assert statements to help the prover. |
Reading Counterexample Traces
Run with --trace to get a counterexample when verification fails:
openjml --esc --trace FileName.java
The trace shows concrete values that violate the spec. Use these to understand exactly which execution path causes the failure.
8. Common Pitfalls
Each entry shows the mistake, why it fails, and the fix.
Pitfall 1: Multiple assignable Clauses (Intersection, Not Union)
// WRONG -- computes intersection, which is \nothing
//@ assignable x;
//@ assignable y;
// FIX -- single clause with both
//@ assignable x, y;
Pitfall 2: Loop Invariant Excludes Exit Value
// WRONG -- fails LoopInvariantBeforeLoop when i == a.length at exit
//@ maintaining 0 <= i < a.length;
// FIX -- include the exit value
//@ maintaining 0 <= i <= a.length;
Pitfall 3: Missing Loop Spec Part
OpenJML requires all three loop spec clauses. Omitting any one causes failures or unsoundness.
// WRONG -- missing loop_writes and decreases
//@ maintaining 0 <= i <= n;
for (int i = 0; i < n; i++) { ... }
// FIX -- all three parts
//@ maintaining 0 <= i <= n;
//@ loop_writes i, otherVars;
//@ decreases n - i;
for (int i = 0; i < n; i++) { ... }
Pitfall 4: requires Ordering Breaks Well-Definedness
// WRONG -- a[i] dereference may be undefined if a is null
//@ requires 0 <= i < a.length;
//@ requires a != null;
// FIX -- null check first
//@ requires a != null;
//@ requires 0 <= i < a.length;
Pitfall 5: Forgetting assignable Defaults to \everything
If you omit assignable, OpenJML assumes assignable \everything, which means every field
and array is considered modified. This destroys all knowledge about unchanged state after the
method call, causing downstream verification failures.
// WRONG -- no assignable means \everything
//@ ensures \result == x + 1;
public int increment(int x) { return x + 1; }
// FIX -- declare it pure or add assignable \nothing
//@ ensures \result == x + 1;
//@ assignable \nothing;
public int increment(int x) { return x + 1; }
// Or better:
//@ ensures \result == x + 1;
public /*@ pure @*/ int increment(int x) { return x + 1; }
Pitfall 6: Using Impure Methods in Spec Expressions
// WRONG -- size() is not declared pure, so it cannot appear in a spec
//@ ensures \result == size() - 1;
// FIX -- declare size() as pure
//@ ensures \result >= 0;
public /*@ pure @*/ int size() { return count; }
// Now this works:
//@ ensures \result == size() - 1;
Pitfall 7: Forgetting JML Non-Null Default
// WRONG -- JML assumes s is non-null, but caller might pass null
public int length(String s) {
if (s == null) return 0;
return s.length();
}
// FIX option A -- add nullable annotation
public int length(/*@ nullable @*/ String s) { ... }
// FIX option B -- add requires (if null is truly forbidden)
//@ requires s != null;
public int length(String s) { ... }
Pitfall 8: Called Method's Frame Clobbers Caller's State
// Called method has no assignable clause (defaults to \everything)
public void helper() { ... }
// Caller's spec fails because helper() may modify anything
//@ ensures field == \old(field) + 1;
public void caller() {
field++;
helper(); // OpenJML assumes helper() may have changed field
}
// FIX -- add assignable to helper()
//@ assignable \nothing;
public void helper() { ... }
Pitfall 9: normal_behavior with Possible Exceptions
// WRONG -- normal_behavior implies signals (Exception) false,
// but the body may throw ArrayIndexOutOfBoundsException
/*@ public normal_behavior
@ ensures \result == a[i];
@*/
public int get(int[] a, int i) { return a[i]; }
// FIX -- add requires to prevent the exception
/*@ public normal_behavior
@ requires a != null;
@ requires 0 <= i < a.length;
@ ensures \result == a[i];
@*/
public int get(int[] a, int i) { return a[i]; }
9. Specification Strength & Completeness
Weak specifications verify easily but provide little value to callers. Strong specifications enable modular verification -- callers can reason about the method's effect without reading its implementation.
Guidelines
-
Postconditions should fully characterize the result. For a
findmethod, don't just say\result >= -1. Say://@ ensures \result == -1 ==> (\forall int j; 0 <= j < a.length; a[j] != key); //@ ensures \result >= 0 ==> (0 <= \result < a.length && a[\result] == key); -
Frame conditions should be as tight as possible.
assignable \everythingis almost never correct. List exactly what changes. -
Preconditions should be as weak as possible. Don't require more than the method actually needs. Overly strong preconditions reduce the method's usability.
-
Invariants should capture the class's representation property. For example, a sorted array class should have:
//@ invariant (\forall int i; 0 <= i < size - 1; data[i] <= data[i + 1]); -
Every public method should have a spec. Private/package methods need specs when called from a specified public method, because OpenJML verifies modularly -- it uses the callee's spec, not its body.
-
Use
assertto help the prover. If ESC fails on a complex method, insert intermediate//@ assert P;statements to break the proof into smaller steps. -
Ghost variables for abstract state. When the concrete representation is complex, introduce ghost fields to represent abstract state and specify in terms of those:
//@ ghost public int abstractSize; //@ invariant abstractSize == computeSize();
10. Further Reference
- OpenJML Tutorial: https://www.openjml.org/tutorial/ -- Worked examples for all major features, from basic postconditions through ghost variables.
- JML Reference Manual: https://www.openjml.org/documentation/JML_Reference_Manual.pdf -- Complete syntax and semantics for all JML constructs.
- OpenJML User Guide: https://www.openjml.org/documentation/OpenJMLUserGuide.pdf -- Tool options, configuration, and integration with build systems.
- OpenJML GitHub: https://github.com/OpenJML/OpenJML -- Source, issues, and release builds.
Version History
- e0220ca Current 2026-07-05 23:34
