A Brief Guide on How to Read JML

This guide serves to describe the subset of the Java Modeling Language (JML) supported by OpenJML's static checker and is used in specifying NativeJceExtensions. JML has many complexities, as does the task of verifying Java code, so this guide is only meant to acquaint the reader with the contents of JML specifications, rather than necessarily be a fully-fledged guide to verifying complete libraries using OpenJML.

For a more rigorous description of OpenJML, see the JML reference manual: http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_toc.html

Executive Summary

JML allows for annotating Java code with machine-checkable specifications that describe how method calls affect an object's state. OpenJML translates Java files annotated with OpenJML into problems that can be passed to an SMT solver, which will verify if the specifications, invariants, and assertions hold under all possible inputs or will identify counterexamples (or time out).

From the perspective of the Java compiler, JML annotations are simply comments because they are marked off using "//@" for single-line annotations or enclosed between the markers "/@" and "@/" for multiple-line annotations. Without delving into low-level details, anything marked off in a JML annotation can be thought of as either an obligation for the SMT solver to prove about the code or a piece of additional state that exists only in the solver's view of the file (often necessary to express ordering conditions). If OpenJML verifies the JML annotations in a given file, that means that they have been proven to hold for all inputs assuming the stated pre-conditions and barring a Java error.

Below are cursory rules for interpreting JML annotations. The rest of this file describes these constructs in more detail, as well as some others. * Within a method, assert [boolean expr], as aforementioned, tells the solver to check that the expression is true for all inputs (given the preconditions in the specifications). * Within a class, invariant [boolean expr] assumes that the expression is true at the entry point of all methods and requires the solver to prove that it is maintained at all exit points, including when exceptions are thrown. * The most powerful and general JML construct is a specification, which is stated above a method's signature. A normal_behavior specification claims that if the preconditions are met, the postconditions will be true after the method is finished; an exceptional_behavior specification claims that if the preconditions are met, the given types of exceptions will be thrown. The solver assumes the preconditions are true and determines if the method body establishes the postconditions on every return path. When the solver encounters a method call in checking other methods, it will reason about the call only in terms of the method's specification (checks that preconditions are true, then assumes postconditions are true and moves on), regardless of its body. This is the syntax for specifications:

  /*@ public normal_behavior
    @   requires [precondition]; // multiple requires clauses is equivalent to conjunction
    @   assignable [fields modified by the class]; // the method may assign only to fields listed here; the fields should be characterized in the postcondition 
    @   ensures [postcondition]; // multiple ensures is also equivalent to conjunction
    @ also
    @ private exceptional_behavior
    @   requires [precondition]; // should be mutually exclusive with normal_behavior
    @   assignable [fields assigned];
    @   signals ([exception type]) [condition true when that exception is thrown];
    @ also // can chain any number of specifications, checked to be simultaneously true
    @ public exceptional_behavior
    @   requires [other condition];
    @   assignable \nothing; // nothing is assigned
    @   signals_only [exception type]; // if preconditions are true, *only* this type of exception can be thrown
    @*/

Note that if a field is listed in an assignable clause but not described in ensures clauses, OpenJML considers it to have been havoc'd. In formal methods, havoc(x) refers to a function that destroys all information about x, hence if a field is "havoc'd," the verifier assumes no knowledge of its value. This means that OpenJML will treat fields in assignable clauses as having been set to any possible value (none in particular), which is occasionally a desirable specification (e.g., not wanting to make assumptions about the behavior of a callback, perhaps).

The above are the core constructs of JML, but the following describe further useful concepts and annotations that can assist in specifying desired behavior: * Fields and methods can only be referenced in invariants and specifications of the same or a lower privacy level, so a private field can only be referenced in a private specification. However, it is often relevant to discuss the private state of a class in a public specification (e.g., it is hard to analyze a buffer implementation without mentioning the buffer contents), so a variable of a low privacy in Java can be marked spec_public (or spec_protected or spec_private) for it to be treated as public (etc.) wherever JML specifications are concerned. * The annotation pure on a method is equivalent to specifying that it has a specification with the clause assignable \nothing in all visibility levels. Only a pure method can be called inside JML blocks, including specifications. * A class or local variable can be declared within a JML block with the annotation ghost (e.g., //@ public ghost int v;). This variable exists only in the solver's view of the file. A ghost variable can be assigned in JML blocks with the keyword set, e.g., //@ set v = 1; Such variables often correspond to state that the actual implementation does not keep but is necessary for describing a class's behavior, such as a state machine for encoding orderings. For JML's purposes, ghost variables are the same as any other, so they must be included in assignable clauses. * A method may be declared in a JML block with the annotation model, which marks it as a method that can only be used within specifications and assertions. A model method does not need an implementation, as the solver will analyze it only in terms of its specification (the specification is assumed to be true if no body is provided). This is often convenient for making specifications more modular, as repeated conditions can be factored out into a pure model method. * It is also possible to create a model class and to instruct the solver to replace a real type with the model one (if the signatures and specifications are compatible) using the following syntax: public /*@ { ModelType } @*/ RealType method(/*@ { ModelType } @*/ RealType r); * A class field, method argument, or method return type may be annotated with non_null to establish that it should never be null. The solver checks that a non_null field is never assigned null, that null is never passed for a non_null argument, and a method with a non_null return type cannot return null; the solver can assume when verifying methods that non_null fields or variables will never be null. A method or whole class can be marked as non_null_by_default to implicitly add non_null to all method signatures and class fields; in that case nullable can be used to mark exceptions.

Core Language Syntax

All JML assertions and specifications are contained within Java comments that are interpreted by the OpenJML tool, such as the following:

//@ // One line of JML

/*@ // Multiple lines of JML code may follow.
  @ // The @ at the start of a line is optional
  @ // but is good practice.
  @ // Single-line comments within JML blocks are fine. 
  @*/

Conditions and effects of specifications are largely expressed using ordinary Java expressions, emphasized because statements such as if-else blocks and assignments are not allowed. Mutators like ++, +=, etc., are also not allowed.

That is, any given line of JML should be pure; JML allows for discussing methods that mutate state by describing the pre- and post-conditions.

The syntax specific to assertions, method specifications, and other verification-related constructs will be discussed in their respective sections. Here, however, we will note that JML adds new logical operators:

• a ==> b (equivalent to !a || b, including its short-circuiting behavior)
• a <==> b (equivalent to a == b for booleans)
• \forall type i; guard(i); condition(i) (for all values i for which guard(i) is true, condition(i) is true. E.g., \forall int i; 0 <= i && i < buf.length; buf[i] == 0 establishes that buf is 0 in all indices)
• \exists type i; guard(i); condition(i) (for some value of i for which guard(i) is true, condition(i) is also true)

In the case of \forall and \exists, the guard function should ideally establish that the set of possible values of the index be bounded or else the SMT solver may have trouble reasoning about the quantifier.

Note that function calls within specifications are allowed, but any function called must be marked as "pure" in its signature (see the following section).

Specifications

A method is specified in JML by describing its behavior, namely by stating what will be true about the return value and object's state when the method returns normally, what will be true when the method throws an exception, and what field the method is allowed to modify. JML behavior blocks enforce this relationship between preconditions and postconditions so long as no Java Error (e.g., OutOfMemoryError) is raised. (By default, OpenJML also assumes that all methods will terminate.)

OpenJML checks that the implementation of a method fulfills its postconditions given the preconditions and also checks that the preconditions for a method call are fulfilled at each call site.

Note that when OpenJML reasons about method calls, OpenJML will only take the specifications into consideration, never the method bodies, so it is important that specifications express all relevant properties about what a method returns and how it affects the state.

Specification syntax

The syntax for a general specification is as follows:

/*@ [privacy] behavior
  @   requires [boolean expr];
  @   // any number of requires clauses
  @   assignable [list of fields that could be assigned];
  @   ensures [boolean expr];
  @   // any number of requires clauses
  @   signals ([Exception type] e) [boolean expression];
  @   // any number of signals clauses
  @*/

The requires clauses state the preconditions for the specification, meaning that the rest of the specification only applies if these conditions are met at the call site (the preconditions are also assumed when checking that the method body satisfies the specification).

The ensures clauses state the postconditions that hold when the method returns (and thus do not apply if an exception is thrown). The ensures clauses are checked at all return sites, meaning that if a field can have different values on different execution paths, then the ensures clauses cannot assume any particular one has been followed. If different control paths need to be specified, it would be best to make the predicates conditional, e.g., ensures A ==> B. Note that if a function has a non-void return type, \result can be used like an ordinary variable in ensures clauses to refer to the return value.

A series of requires or ensures clauses is equivalent to a single requires clause or ensures clause with the conjunction of all the predicates expressed within the separate clauses.

The assignable clause holds that only the fields listed can be modified by the method. It is up to the ensures clauses to describe what the values of modified fields will be; otherwise, OpenJML will assume the value has been havoc'd. (Assignability will be discussed in more detail below.) Having multiple assignable clauses in a single specification is the equivalent of a single assignable clause with all fields listed.

The signals clauses serve to describe the behavior when the method throws an exception. A signals clause states that if an exception of the type specified is thrown, the listed condition should be true in the catch block if that exception is caught. For example:

signals (InvalidArgumentException e) e.getMessage() == "Tough luck";

Note that the exception does not need to be bound to a variable, so the following is also a valid signals clause:

signals (IllegalArgumentException) x < 0;

A signals clause may only refer to classes that inherit from java.lang.Exception, not other Throwable classes (e.g., java.lang.Error).

normal_behavior specifications

Most often, it is convenient to discuss a specification in terms of a function's behavior when an exception is not thrown. A normal_behavior specification thus is syntactic sugar for a behavior block with the clause signals (Exception) false; to signify that if the preconditions are met, no exception can be thrown. Here is a simple example:

  /*@ public normal_behavior
    @   requires arr != null && 0 <= x && x < arr.length;
    @   assignable \nothing;
    @   ensures \result == arr[x];
    @*/
  public int access(int[] arr, int x) {
      return arr[x];
  }

exceptional_behavior specifications and more on signals clauses

The opposite of normal_behavior is exceptional_behavior, which asserts that if all the preconditions are true, the method must throw an exception. This is equivalent to a general behavior specification with the clause ensures false; to guarantee that it the method, under these circumstances, cannot return normally.

Because signals clauses only describe a condition that holds when that particul