JML

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

The relevant knowledge for this evaluation 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 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 and exceptional_behavior are used to specify that a method should terminate normally without a thrown exception or exceptionally otherwise. Keyword requires followed by a boolean expression defines a precondition while ensures also followed by a boolean expression defines a postcondition. An expression is basically a normal Java expression as used for instance in if statements. But additionally the implication operator ==> and quantifiers (e.g. \forall) can be used.

The ensures clause makes a statement about the final state after method execution. To express changes relative to the prestate before method invocation, the keyword \old can be used. Keyword \result is used to refer to the method return value.

The last part of a method contract is the assignable clause. It lists all locations the method is allowed to change. Keyword \nothing expresses that the method is not allowed to change any location.

Consider the following example. The method contract of addCredits says that the method should be called in a state in which credits is greater than zero (requires). Then the method will guarantee that no exception is thrown (normal_behavior) and that the value of acquiredCredits is increased by credits (first ensures). It also guarantees that the returned value is the new value of acquiredCredits (second ensures). At last, the assignable clause says that only acquiredCredits and no other locations like firstname or surname are allowed to be changed by the method.

public class Student {
   private /*@ nullable @*/ String firstname;
   
   private /*@ non_null @*/ String surname;

   private int acquiredCredits = 0;
   
   /*@ normal_behavior
     @ requires credits > 0;
     @ ensures acquiredCredits == \old(acquiredCredits) + credits;
     @ ensures \result == acquiredCredits;
     @ assignable acquiredCredits;
     @*/
   public int addCredits(int credits) {
      acquiredCredits += credits;
      return acquiredCredits;
   }
}

For method parameters as well as for instance and class fields with a reference type its ability to be null needs to be specified. Keyword nullable allows the null value while non_null forbids it. In the example above, firstname might be null while surname will be never null.

3 Class Invariants

An 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. Technically, an invariant can be seen as pre and postcondition added to all method contracts.

Let us add the following invariant to class Student. It says that the value of acquiredCredits is never negative.

/*@ invariant acquiredCredits >= 0;
  @*/
private int acquiredCredits = 0;

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 restricts with the first loop invariant the range of index variable i. The second loop invariant ensures that all already visited array elements are assigned with the array index. Termination can be proven with help of the array length and the index variable (decreasing term). Finally, the loop can change all fields of array (but not array itself) and i.

public static void fillArray(int[] array) {
   /*@ loop_invariant i >= 0 && i <= array.length;
     @ loop_invariant (\forall int j; j >= 0 && j < i; array[j] == j);
     @ decreasing array.length - i;
     @ assignable array[*], i;
     @*/
   for (int i = 0; i < array.length; i++) {
      array[i] = i;
   }
}

5 Aliasing and Assignable

Listed instance fields in the assignable clause give the right to change its values independent from the way how the object is accessed.

Consider for instance the following example. The parameters a and b are aliased (they point to the same object) as expressed by the precondition a == b. The implementation fulfills the specification, although the specification allows only to change instance field acquiredCredits on b while the implementation changes it on a.

/*@ normal_behavior
  @ requires a == b;
  @ assignable b.acquiredCredits;
  @*/
public static void doNothing(Student a, Student b) {
   a.acquiredCredits = b.acquiredCredits;
}

6 From JML to Java Dynamic Logic

To verify if a Java program adheres to its JML specification, KeY translates both into a formula in Java Dynamic Logic. Java Dynamic Logic is also used by the Symbolic Execution Debugger (SED) to present results.

This section gives a short introduction about how to read Java Dynamic Logic.

For the actual verification, KeY uses a Gentzen-style sequent calculus. The main data structure of such a calculus is a sequent like the following:


         A, B ==> C, D
         
It can be read as: Assuming that all formulas on the left side (A and B) of the sequent arrow ==> hold, at least one formula on the right side (C or D) needs to hold. The left side contains typically preconditions to assume while the right side contains postconditions to be proven.

6.1 Method Contracts in Java Dynamic Logic

The following figure shows on the left the source code from Section 2 Method Contracts and on the right the initial sequent generated by KeY to verify the correctness of method addCredits. Boxes are used to map the Java/JML constructs to their representation in Java Dynamic Logic.

6.2 Loop Invariants in Java Dynamic Logic

The following figure shows on the left the source code from Section 4 Loop Invariants and on the right the sequent generated by KeY to verify that the loop invariant is preserved by loop guard and body. Boxes are used to map the Java/JML constructs to their representation in Java Dynamic Logic.