openjml-more

name	openjml-more
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. (more details)

JML Specification & OpenJML Verification

This is expert guidance when using 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 (--esc or --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
  @*/

Code formatter compatibility: Java code formatters (Palantir Java Format, Google Java Format, etc.) will silently convert //@ to // @ by inserting a space after //. The result is a plain Java comment that OpenJML completely ignores -- no warning is emitted, and the annotation simply has no effect. This silently disables skipesc, assume, assert, invariants, and any other single-line JML annotation.

Always prefer /*@ ... @*/ block-comment style when the project uses an automated code formatter. Block comments are not reformatted by standard Java formatters. This applies to all JML annotations, including short ones:

// WRONG -- formatter will break this into "// @ skipesc"
//@ skipesc

// SAFE -- block comment survives formatting
/*@ skipesc @*/

// SAFE -- inline modifiers in block comments also survive
private /*@ spec_public @*/ int count;
public /*@ pure @*/ int size() { return count; }

If you must use single-line style, configure the formatter to exclude JML comments (e.g., Spotless toggleOffOn tags) or verify that annotations survive after running the formatter.

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 exception types (checked or unchecked) may be thrown
also	Separates multiple specification cases; also joins inherited specs when overriding a method (see Section 13)
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 in every visible state: at the end of construction, and at the entry and exit of every non-helper public method (including inherited methods). See JML's visible-state semantics.
constraint P;	History constraint: relates pre- and post-state across method calls
initially P;	Must hold at the end of every constructor
static_initializer	Specifies the static { } initializer block. Must be placed immediately before it. Supports ensures clauses for static field initialization.

Example of static_initializer:

public static final Comparator<Event<?>> ORDERING;

/*@ public static_initializer
  @   ensures ORDERING != null;
  @*/
static {
    ORDERING = Comparator.comparingLong(Event::time)
                         .thenComparingLong(Event::sequence);
}

Note: Lambdas inside static initializer blocks can trigger OpenJML internal errors ("NULL SYMBOL") when verified together with other files. If this occurs, add /*@ skipesc @*/ before the static block.

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 (usable in any loop spec clause: maintaining, decreases, loop_writes)

Store-ref syntax for frame conditions:

Syntax	Context
a[i]	Single array element (in assignable / loop_writes)
a[*]	All elements of array a
a[i..j]	Array elements from index i to j (store-ref syntax for assignable / loop_writes only; not a general spec expression)

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 spec expressions. Implies assignable \nothing;. This is the standard modifier required to call a method inside a JML annotation.

• spec_pure: Like pure but applies only during verification (no RAC runtime check). Still requires the method to be side-effect-free for specification purposes. Use pure unless you specifically need to suppress the RAC instrumentation.

• 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 reference types in declarations to non-null. (Array element nullity depends on the element type declaration; see Section 4 for visibility implications.)

• nullable_by_default: Class-level modifier to flip the default for all declarations in the class.

• helper: Exempts a constructor or method from class invariant checking at entry and exit. Normally, invariants must hold at the end of every constructor and at the entry/exit of every public method. Marking a method helper removes this obligation, which is useful when:

  • OpenJML cannot prove field assignments establish invariants in a constructor (a known prover limitation with some constructor forms).
  • An internal method is called in a state where invariants are temporarily broken.

  When using helper, try these approaches in order before resorting to skipesc:

  1. First try: verify without skipesc. Write the constructor spec and run ESC. OpenJML can prove constructor invariants for many simple field assignments.
  2. Then try: add intermediate //@ assert statements inside the constructor body to guide the prover through field-by-field invariant establishment.
  3. Then try: use targeted //@ assume statements for the specific invariant clause the prover struggles with. Document the reason (e.g., "OpenJML limitation: cannot prove field assignment establishes invariant through generic type parameter").
  4. Last resort: apply skipesc. Ensure the constructor still has a full JML contract (requires, ensures for each field assignment) so the factory method and callers can reason about it modularly.

  See Section 16 (Verification Escalation) for the full decision process.

  The standard pattern when skipesc is unavoidable is to mark the constructor helper and provide a public factory method that calls it. The factory method uses the constructor's postconditions to prove the invariants hold on the returned object:

  /*@ requires initialState != null;
    @ ensures field == initialState;
    @*/
  /*@ skipesc @*/  // last resort -- only after assert/assume alternatives fail
  private /*@ helper @*/ MyClass(S initialState) {
      this.field = initialState;  // OpenJML may fail to prove this establishes invariants
  }
  
  /*@ public behavior
    @   requires initialState != null;
    @   ensures \result != null;
    @*/
  public static <S> MyClass<S> create(S initialState) {
      return new MyClass<>(initialState);  // invariants proven from constructor's spec
  }
  

---

4. Visibility Rules

JML enforces Java-like visibility on specifications. A specification clause can only reference identifiers that are at least as visible as the method or class being specified.

The Core Rule

• A public method's spec can only reference public fields, public pure methods, and public model fields.
• A protected method's spec can reference protected or public members.
• Package-private and private follow analogously.

Problem: Public API, Private Representation

You often need to specify a public method in terms of private fields. Three solutions:

1. spec_public / spec_protected (quick fix):

private /*@ spec_public @*/ int count;

//@ ensures \result == count;
public /*@ pure @*/ int size() { return count; }

This exposes the private field to public specs. Use sparingly -- it leaks implementation details.

2. Model fields (preferred for abstraction):

//@ public model int size;
//@ private represents size = count;

//@ ensures \result == size;
public /*@ pure @*/ int size() { return count; }

See Section 5 for full details on model fields.

3. Public pure methods as abstraction:

Specify in terms of other public pure methods rather than fields:

//@ ensures \result >= 0;
public /*@ pure @*/ int size() { return count; }

//@ ensures size() == \old(size()) + 1;
public void add(Object o) { ... }

Common Violation

private int[] data;

// WRONG -- public spec references private field
//@ ensures \result == data[i];
public int get(int i) { return data[i]; }

// FIX -- use spec_public or a model field
private /*@ spec_public @*/ int[] data;

OpenJML reports visibility violations as compile errors, not verification failures.

---

5. Model Fields, Ghost Fields, and represents

JML provides two kinds of specification-only fields for abstracting over implementation details.

Model Fields

A model field exists only in the specification. It has no runtime storage. You define it with model and connect it to the implementation with a represents clause:

public class Stack {
    private Object[] elems;
    private int top;

    //@ public model int size;
    //@ private represents size = top;

    //@ public model boolean isEmpty;
    //@ private represents isEmpty = (top == 0);

    //@ public invariant size >= 0;

    //@ ensures size == \old(size) + 1;
    //@ assignable size;
    public void push(Object o) { elems[top++] = o; }
}

Key points:

• Model fields are declared with a visibility (public model int size;).
• The represents clause maps the model field to a concrete expression.
• The represents clause must be at least as visible as the fields it reads (typically private represents).
• Use model fields in assignable clauses to abstract frame conditions.
• OpenJML checks that the represents mapping is consistent with the spec.

Ghost Fields

A ghost field is a specification-only variable that you assign to explicitly in ghost statements. Unlike model fields, ghost fields have no represents clause -- you manage their value directly:

public class Counter {
    //@ ghost public int specCount = 0;

    //@ assignable specCount;
    //@ ensures specCount == \old(specCount) + 1;
    public void increment() {
        count++;
        //@ set specCount = specCount + 1;
    }
}

When to Use Which

Use case	Mechanism
Abstract a concrete field for public specs	Model field + represents
Track specification-only state (e.g., call count, protocol state)	Ghost field + set
Hide representation from callers	Model field
Need explicit control over value in proof	Ghost field

---

6. 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 pure and focus on ensures.
• Is this a command (modifies state)? Focus on assignable + ensures.
• Can it throw exceptions? Plan signals / signals_only clauses.

Choosing behavior vs normal_behavior: If the method body contains any throw statement -- even in guard clauses like Objects.requireNonNull(), if (x < 0) throw ..., or validation checks -- use behavior, not normal_behavior. This is the most common case for public API methods that validate their inputs.

normal_behavior implies signals (Exception e) false;, so OpenJML will report a verification failure on any method that can throw, even if the throw is unreachable given the preconditions. behavior is always safe; normal_behavior is an optimization that adds an implicit no-exceptions guarantee. Only use normal_behavior when you are certain the method cannot throw under any circumstance (pure getters, simple computations with tight preconditions, etc.).

Step 2: Annotate Nullness

• JML defaults to non_null for reference types in declarations.
• 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 requires clauses are conjoined (AND).

Step 4: Write Frame Conditions (assignable)

• List every field and array element that the method may modify.
• Use exactly ONE assignable clause per spec case. Multiple assignable clauses 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[*]; or assignable a[i..j];.
• For abstract state: you can list model fields in assignable (see Section 5).

Step 5: Write Postconditions (ensures)

• Describe the return value with \result.
• Describe state changes using \old(expr) to reference pre-state values.
• Multiple ensures clauses are conjoined (AND).
• Make postconditions strong enough for callers to reason about the result (see Section 14).

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 (checked and unchecked).
• For methods that never throw: signals (Exception e) false; or use normal_behavior.

Step 7: Write Loop Specifications (if applicable)

In practice, OpenJML needs all three loop spec clauses to verify a loop successfully. Omitting any one typically causes verification failures or unsound results:

1. 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
2. loop_writes: Every variable or array element modified in the loop body
3. decreases: An integer expression that strictly decreases each iteration

Step 8: Verify and Iterate

1. Run openjml --esc FileName.java
2. If verification fails, read the failure name and line number
3. Consult Section 11 (failure remediation table) and Section 12 (common pitfalls)
4. Fix the spec or code, then re-verify
5. Repeat until exit code 0

---

7. 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}; @*/

    ...
}

---

8. Running OpenJML

Extended Static Checking (Primary)

openjml --esc FileName.java

• Exit code 0: All specifications verified.
• Exit code 1: Parse errors, type errors, or JML syntax errors. The file did not compile. Read the compiler diagnostics to fix these before attempting verification.
• Exit code 6: One or more verification failures. Read output for failure names and locations.
• Other exit codes: Tool issues or configuration problems.

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
--subexpressions	Show values of subexpressions in counterexample traces (use with --trace)
--counterexample / -ce	Request a counterexample from the solver (more detail than --trace alone)
--check-feasibility=all	Check that each spec is satisfiable (detects vacuously true specs)
--progress	Show progress during verification
--sourcepath=dir	Add source path for dependent files
--specspath=dir	Add path to spec files (.jml); see Section 9
--classpath=path	Set classpath for dependencies
--code-math=MODE	Arithmetic mode for code (see Section 10)
--spec-math=MODE	Arithmetic mode for specs (see Section 10)

Debugging Aids in Specs

In addition to command-line flags, JML provides in-spec debugging:

//@ show expr;   // prints the value of expr during RAC, shows value in ESC traces
//@ assert P;    // intermediate assertion to narrow down where proofs fail

Runtime Assertion Checking

RAC compiles JML specifications into runtime checks embedded in the bytecode, then executes the program. It is a two-step process:

Step 1 -- Compile with RAC instrumentation:

openjml --rac FileName.java

This produces .class files with embedded assertion checks. Any JML annotation that cannot be compiled (e.g., quantifiers over infinite domains) is silently skipped.

Step 2 -- Run the instrumented class:

openjml --rac-run ClassName

This executes the class and reports any JML assertion violations at runtime, with the source location and failing clause.

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.

---

9. Specification Files (.jml)

JML specifications can be placed in separate .jml files instead of (or in addition to) inline annotations in .java files.

When to Use .jml Files

• Specifying library code you cannot modify
• Keeping specs separate from implementation for organizational reasons
• Providing specs for third-party APIs

File Structure

A .jml file mirrors the .java file's structure but contains only declarations and JML annotations. Method bodies are replaced with ;:

// File: Stack.jml
public class Stack {

    //@ public model int size;

    //@ ensures size == \old(size) + 1;
    //@ assignable size;
    public void push(Object o);

    //@ ensures \result == size;
    public /*@ pure @*/ int getSize();
}

Search Order

OpenJML searches for specs in this order:

1. .jml file on the specs path (--specspath)
2. .jml file on the source path (--sourcepath)
3. Inline annotations in the .java file

Critical rule: If a .jml file is found, its specifications completely replace any inline JML annotations in the corresponding .java file. The inline annotations are silently ignored. This is the most common source of confusion when using .jml files -- if your inline specs seem to have no effect, check whether a .jml file exists on the search path.

Specifying the Specs Path

openjml --esc --specspath=specs src/Main.java

---

10. Arithmetic Modes

Integer arithmetic in Java can overflow silently. JML and OpenJML provide three arithmetic modes that control how overflow is handled during verification.

The Three Modes

Mode	Behavior
java_math	Java semantics: arithmetic wraps on overflow (mod 2^32 / 2^64). No overflow warnings.
safe_math	Java semantics, but OpenJML warns if an operation might overflow.
bigint_math	Mathematical integers: no overflow possible. All int/long values are treated as unbounded.

Defaults

• Code defaults to safe_math: Java wrap semantics, but overflow generates a verification warning (ArithmeticOperationRange).
• Spec expressions default to bigint_math: specs use true mathematical integers, so \old(x) + 1 never overflows in a spec context.

Setting Modes

Per-file or per-class (JML annotation):

//@ code_java_math
//@ code_safe_math
//@ code_bigint_math
//@ spec_java_math
//@ spec_safe_math
//@ spec_bigint_math

Command-line (applies globally):

openjml --esc --code-math=java FileName.java    # suppress overflow warnings
openjml --esc --code-math=safe FileName.java     # warn on overflow (default)
openjml --esc --code-math=bigint FileName.java   # treat code as unbounded math

Practical Guidance

• If you get ArithmeticOperationRange warnings and the overflow is intentional (e.g., hash functions), use //@ code_java_math on that method or pass --code-math=java.
• If you want to prove absence of overflow, keep the default safe_math and add preconditions that bound inputs tightly enough to prevent overflow.
• Spec expressions rarely need mode changes since bigint_math is the natural choice for mathematical reasoning.

---

11. 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.
PossiblyNullAssignment	Assigning a possibly-null value to a non-null location	A nullable expression is assigned to a field, parameter, or return declared non-null	Add a null check before assignment, or make the target nullable, or prove the value is non-null via preconditions.
PossiblyNullReturn	Method may return null but return type is non-null	Implementation has a code path returning null, or a called method's return is nullable	Add requires to prevent the null path, annotate return as nullable, or fix the implementation.
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.
LoopDecreasesNonNegative	decreases expression is negative at some point during the loop	The variant function goes below zero before the loop exits	Tighten the loop invariant to ensure the decreases expression stays non-negative, or fix the variant.
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.
Constraint	History constraint violated	A constraint clause relating pre- and post-state is not satisfied after a method call	Fix the implementation to maintain the constraint, or weaken the constraint.
Initially	initially clause not established	Constructor does not establish the initially condition	Ensure all constructors establish the required initial condition.
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 under safe_math (the default)	Add preconditions bounding inputs, cast to long before computing, or set //@ code_java_math if overflow is intentional. See Section 10.
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.

For richer output, combine flags:

openjml --esc --trace --subexpressions -ce FileName.java

This shows counterexample values for every subexpression, making it easier to pinpoint which part of a complex spec or computation is failing.

Detecting Vacuous Specs

A spec can verify trivially if its precondition is unsatisfiable (no valid inputs exist). Use feasibility checking to detect this:

openjml --esc --check-feasibility=all FileName.java

This reports a warning for any method whose precondition is infeasible, meaning the spec is vacuously true and provides no real guarantee.

---

12. 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 needs all three loop spec clauses to verify successfully. Omitting any one causes failures or allows unsound reasoning.

// 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]; }

Pitfall 10: Visibility Mismatch in Specs

// WRONG -- public spec references private field
private int count;
//@ ensures \result == count;
public /*@ pure @*/ int size() { return count; }

// FIX -- use spec_public
private /*@ spec_public @*/ int count;
// Or use a model field (see Section 5)

---

13. Specification Inheritance

When a class overrides a method from a parent class or interface, JML specs are inherited and combined automatically.

How It Works

• The overriding method inherits all specification cases from the parent.
• If the overriding method adds its own specs, they are joined with the parent's specs using also semantics.
• Preconditions are weakened (disjoined): the overriding method must accept at least the same inputs as the parent.
• Postconditions are strengthened (conjoined): the overriding method must satisfy both its own and the parent's postconditions (for the relevant spec case).
• This enforces behavioral subtyping (Liskov Substitution Principle).

Example

public class Shape {
    //@ requires scale > 0;
    //@ ensures \result >= 0;
    public /*@ pure @*/ double area(double scale) { ... }
}

public class Circle extends Shape {
    /*@ also
      @   requires scale > 0;
      @   ensures \result == Math.PI * radius * radius * scale;
      @*/
    public /*@ pure @*/ double area(double scale) { ... }
}

The also keyword is required when the overriding method adds specification cases. OpenJML verifies that Circle.area satisfies both Shape's postcondition (\result >= 0) and its own (\result == Math.PI * radius * radius * scale).

Key Points

• You do NOT need to repeat the parent's spec in the child -- it is inherited automatically.
• Use also at the beginning of the child's spec to add additional cases.
• If you omit also, OpenJML treats the child's spec as standalone, which may silently lose the parent's contract. Always use also when overriding a specified method.
• Interface method specs are inherited the same way.

---

14. 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

1. Postconditions should fully characterize the result. For a find method, 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);
   

2. Frame conditions should be as tight as possible. assignable \everything is almost never correct. List exactly what changes. Use model fields in assignable to abstract frame conditions (see Section 5).

3. Preconditions should be as weak as possible. Don't require more than the method actually needs. Overly strong preconditions reduce the method's usability.

4. 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]);
   

5. 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.

6. Use assert to help the prover. If ESC fails on a complex method, insert intermediate //@ assert P; statements to break the proof into smaller steps.

7. Use model fields for abstract state. When the concrete representation is complex, introduce model fields (Section 5) to represent abstract state. This keeps public specs independent of the implementation and supports clean specification inheritance:

   //@ public model int size;
   //@ private represents size = elementCount;
   //@ public invariant size >= 0;
   

   Ghost fields are an alternative when you need explicit control over value assignments (e.g., tracking protocol state), but model fields are preferred for representation abstraction.

---

15. Limitations

OpenJML is a powerful tool but has known limitations. Being aware of these avoids wasted debugging time.

• Generics: Partially supported. Complex generic types, wildcards, and bounded type parameters may cause verification failures or tool errors.

• Enums: Basic enum usage works, but complex enum patterns (abstract methods on enum constants, enum with generics) may not verify.

• Varargs: Limited support. Methods with varargs (T... args) may not verify correctly.

• Concurrency: JML and OpenJML do not support concurrent reasoning. Specs assume single-threaded execution.

• Library specifications: OpenJML ships specs for parts of java.lang and java.util, but coverage is incomplete. Missing library specs cause UndefinedCalledMethodPrecondition or weak reasoning. You may need to provide your own specs via .jml files (Section 9).

• Lambda expressions and streams: Limited or no support. Avoid using lambdas in code that needs verification, or isolate them behind specified wrapper methods.

• Records: Java records have several OpenJML quirks:

  • Record accessor methods (e.g., event.time()) may not resolve correctly in invariant or ensures clauses. Prefer direct field references where possible.
  • Record constructors work best with public behavior rather than normal_behavior, since the compact constructor form has implicit field assignments that OpenJML may not fully model.
  • Constructor assignable clauses on records cannot reference this (implicit or explicit) -- OpenJML rejects them with parse errors. Omit assignable from record constructor specs.

• PriorityQueue and collections with incomplete specs: PriorityQueue.add() has assignable values in its library spec, but the prover may treat it as modifying everything, destroying all field knowledge in the caller. PriorityQueue.peek() references internal model methods (_get(0)) with preconditions that cannot be proven externally. PriorityQueue.remove(), queue.isEmpty(), ArrayList.add(), List.copyOf(), and iterator-based for-each loops all have similar spec gaps. When a method uses these collection operations, try these approaches in order:

  1. Use ghost/model fields or //@ assume after the collection call to re-assert facts the prover lost. For example, after queue.add(x), add //@ assume this.otherField == \old(this.otherField); for fields the collection call could not have modified. This preserves ESC verification of the rest of the method.
  2. Extract the collection operation into a small private helper method with its own spec (requires/ensures/assignable). Mark only the helper skipesc, keeping ESC active on the main method that calls it. This localizes the unverifiable code to the smallest possible surface.
  3. Last resort: mark the entire method skipesc. Always provide a full JML contract (requires, ensures, assignable) so callers can still reason about it modularly.

  See Section 16 (Verification Escalation) for the full decision process.

When hitting a limitation, work through the escalation ladder in Section 16 before resorting to skipesc.

---

16. Verification Escalation: When ESC Fails

When OpenJML ESC cannot verify a method, work through these steps in order. Stop as soon as verification succeeds. Each step trades some verification rigor for practicality; the goal is to minimize how much you give up.

1. Fix the spec or code. Most ESC failures are real spec/implementation mismatches. Consult Section 11 (failure table) and Section 12 (common pitfalls) before assuming a tool limitation. Check for: overly strong postconditions, missing preconditions, incomplete assignable clauses, wrong loop invariant bounds, and visibility mismatches.

2. Add intermediate //@ assert statements. Break the proof into smaller steps. The prover may succeed on each sub-goal even when it fails on the whole method. Place asserts after key operations to confirm intermediate state.

3. Simplify the code. Refactor to avoid unsupported features (lambdas, streams, complex generics). Extract the problematic construct into a small helper method so verification difficulty is isolated.

4. Use model or ghost fields. Aid the proof with additional data and logic. The prover can often succeed when the problem is broken apart further. Additional data and logic provides necesary visibility into additional state or spec tracking.

5. Use //@ assume for specific facts. When the prover cannot derive a fact due to incomplete library specs or tool limitations, assert it with assume. Requirements:

   • Keep each assume as narrow and specific as possible.
   • Always add a comment explaining why the assume is needed and what limitation it works around.
   • Prefer assume over skipesc because it preserves ESC verification of the rest of the method -- only the assumed fact is taken on trust.

6. Extract and isolate with skipesc on a helper. When a single operation (e.g., a library call with incomplete specs) poisons the proof for the entire method, extract it into a small private helper method with its own JML contract. Mark only the helper skipesc. The calling method retains full ESC coverage and reasons about the helper through its contract.

7. Use RAC instead of ESC. For methods where ESC times out or hits fundamental tool limitations, runtime assertion checking (--rac / --rac-run) can still validate specs against concrete executions during testing.

8. Apply skipesc to the method as a last resort. When no other technique works, mark the method skipesc. Requirements when using skipesc:

   • The method must still have a full JML contract (requires, ensures, assignable) so callers can reason about it modularly.
   • Add a comment documenting what was tried and why skipesc is necessary.
   • Consider RAC coverage for the skipped method to retain some validation.

Never start at step 8. The steps above are ordered from most rigorous to least. Jumping to skipesc early silently removes a method from formal verification and can mask real bugs.

---

17. 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.