JML

The Java Modeling Language (JML) is a specification language used to specify the expected behavior of Java modules.

Some examples of this evaluation will contain some JML specifications to make the expected behavior more precise. The relevant knowledge about JML is explained in the following sections. Please read them carefully before you continue. If you are familiar with JML, you can skip sections you know well.

1 JML Comments

JML specifications are placed as special comments within the Java source code. Such comments have to start with the @ character. JML comments used in this evaluation look as follows:

/*@ ...
  @ ... 
  @*/

2 Class Invariants

A class invariant is a property used to limit the possible state space of instances. All constructors of a class have to establish the invariant while all methods have to preserve it. It can only be broken temporary within a method execution.

In JML keyword invariant followed by a boolean expression defines a class invariant. An expression is basically a normal Java expression as used for instance in if statements. But additionally quantifiers (e.g. \forall) can be used.

The ability of a reference type to be null can be directly specified using keywords nullable and non_null. An array reference specified as nullable/non_null forces also that the values at all array indices are nullable/non_null.

Consider the following example. The state space of instance field value is limited to positive values (invariant value >= 0;). Additionally, description might be null while id will be never null.

class Entry {
   /*@ invariant value >= 0;
     @*/
   protected int value;

   protected /*@ nullable @*/ String description;

   protected /*@ non_null @*/ String id;
}

3 Method Contracts

A method contract specifies the expected behavior of a method in terms of pre- and postconditions. Assuming that the precondition is fulfilled when the method is called, the method guarantees that the postcondition is established when it returns. In JML the keywords normal_behavior is used to specify that a method should terminate normally without a thrown exception. Keyword requires followed by a boolean expression defines a precondition while ensures also followed by a boolean expression defines a postcondition.

Declaring a method as helper also allows to call the method in a state in which the class invariant does not hold. Such a helper method also does not need to reestablish the class invariant before it is returned.

The last part of a method contract is the assignable clause. It lists all locations the method is allowed to change. Keyword \everything expresses that the method is allowed to change all reachable locations.

Consider the following example. The method contract of accumulate says that the method can be called in any state (requires true;) even if the class invariant does not hold (helper). The method will guarantee only true (ensures true;) which means roughly that the behavior of the method is not specified. A possible implementation can change any location (assignable \everything). The only specified restriction is that no exception will be thrown (normal_behavior).

interface Accumulator {
   /*@ normal_behavior
     @ requires true;
     @ ensures true;
     @ assignable \everything;
     @*/
   public /*@ helper @*/ int accumulate(int accumulation, Entry entry);
}

4 Loop Invariants

A loop invariant is a property which needs to hold before a loop is entered and which is preserved by each loop iteration (loop guard and loop body). Thus it also holds after the loop.

A loop invariant in JML consists of three parts:

The following example realizes a database consisting of Entry instances. The class invariant says that instance field entries is never null and of type Entry[] and also that all contained Entry instances are also not null.

The loop invariant in the example restricts the range of index variable i. Termination of the loop can be proven with help of the array length and the index variable (decreasing term). Finally, the loop is only allowed to change local variables accumulation and i.

public class Database {
   /*@ invariant entries != null;
     @ invariant \typeof(entries) == \type(Entry[]);
     @ invariant (\forall int i; i >= 0 && i < entries.length; entries[i] != null);
     @*/
   private Entry[] entries;

   public Database(Entry[] entries) {
      this.entries = entries;
   }

   /**
    * Accumulates the value of all {@link Entry} instances in the {@link Database}
    * with help of the given {@link Accumulator}.
    * @param accumulator The {@link Accumulator} to use which is not allowed to be {@code null}.
    * @return The computed accumulation.
    */
   public int accumulateDatabase(/*@ non_null @*/ Accumulator accumulator) {
      int accumulation = 0;
      /*@ loop_invariant i >= 1 && i <= (entries.length + 1);
        @ decreasing entries.length - i;
        @ assignable accumulation, i;
        @*/
      for (int i = 1; i <= entries.length; i++) {
         accumulator.accumulate(accumulation, entries[i]);
      }
      return accumulation;
   }
}