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.
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:
/*@ ...
@ ...
@*/
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;
}
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);
}
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:
loop_invariant
is used to specify a loop invariant.decreasing
specifies a value which is always positive and strictly decreased in each loop iteration. It is used to prove termination of the loop. The decreasing clause is also named variant.assignable
limits the locations may changed by the loop.
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;
}
}