JML makes extensions to the Java expression syntax for two purposes.
The main set of extensions are used in predicates.
But there are also some extensions used in
storerefs, which are themselves used in the assignable
,
accessible
, and represents
clauses.
The expressions that can be used as predicates in JML are an extension to the sideeffect free Java expressions. Since predicates are required to be sideeffect free, the following Java operators are not allowed within predicates:
=
),
and the various assignment operators (such as +=
, =
, etc.)
++
and 
),
new
that would call a constructor that is not pure.
Furthermore, within method specification that are not model programs,
one cannot use super
to call a pure superclass method,
because it is confusing in combination with JML's specification inheritance.(28)
We allow the allocation of storage (e.g., using operator new
and pure constructors)
in predicates, because such storage
can never be referred to after the evaluation of the predicate,
and because such pure constructors have no sideeffects other than initializing
the new objects so created.
Also, expressions with side effects are permitted as arguments to
the \duration
and \working_space
expressions, because
their argument expressions are not evaluated.
JML adds the following new syntax to the Java expression syntax, for use in predicates (see the JML Reference Manual [LeavensetalJMLRef] for syntactic details such as precedence):
(* some text describing a Booleanvalued predicate *)have type
boolean
.
Their meaning is either true
or false
,
but is entirely determined by the reader.
Since informal descriptions are notexecutable, they may be treated
differently by different tools in different situations.
==>
and <==
for logical implication and reverse implication.
For example, the formula raining ==> getsWet
is true if either
raining
is false or getsWet
is true.
The formula getsWet <== raining
means the same thing.
The ==>
operator associates to the right, but
the <==
operator associates to the left.
The expressions on either side of these operators must be of type
boolean
, and the type of the result is also boolean
.
<==>
and <=!=>
for logical equivalence
and logical inequivalence, respectively.
The expressions on either side of these operators must be of type
boolean
, and the type of the result is also boolean
.
Note that <==>
means the same thing as ==
for expressions of type boolean
,
and <=!=>
means the same thing as !=
for boolean expressions;
however, <==>
and <=!=>
have a much lower precedence,
and are also associative and symmetric.
<
and <=
to test order of locks.
JML extends these two operators, but not >
and >=
, as
comparisons on Objects. Using synchronized
statements, Java
programs can establish monitor locks to permit only one thread at a
time to execute given sections of code. Any object can be used as
a lock. In order for ESC/Java to
reason about the possibility of deadlocks among threads, a partial order
must be defined on lock objects, with "larger" objects being objects
whose locks should be acquired later. The <
and <=
operators
represent this partial order.
\max
, to provide the "largest" of a set of lock objects. The ordering
used to determine the max is that defined by the <
operator as applied
to objects.
\forall
and \exists
,
which are universal and existential quantifiers (respectively);
for example,
(\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])says that
a
is sorted at indexes between 0 and 9.
The quantifiers range over all potential values of the variables declared
which satisfy the range predicate, given between the semicolons
(;
). If the range predicate is omitted, it defaults to true
.
Since a quantifier quantifies over all potential values of the
variables,
when the variables declared are reference types,
they may be null, or may refer to objects not constructed by the program;
one should use a range predicate to eliminate such cases
if they are not desired.
The type of a universal and existential quantifier is boolean
.
\max
, \min
, \product
, and \sum
,
which are generalized quantifiers that return the maximum, minimum,
product, or sum of the values of the expressions given,
where the variables satisfy the given range.
The range predicate must be of type boolean
.
The expression in the body must be a builtin numeric type,
such as int
or double
; the type of the quantified expression
as a whole is the type of its body.
The body of a quantified expression is the last toplevel expression
it contains; it is the expression following the range predicate,
if there is one.
As with the universal and existential quantifiers,
if the range predicate is omitted, it defaults to true
.
For example, the following equations are all true (see chapter 3 of [Cohen90]):
(\sum int i; 0 <= i && i < 5; i) == 0 + 1 + 2 + 3 + 4 (\product int i; 0 < i && i < 5; i) == 1 * 2 * 3 * 4 (\max int i; 0 <= i && i < 5; i) == 4 (\min int i; 0 <= i && i < 5; i1) == 1For computing the value of a sum or product, Java's arithmetic is used. The meaning thus depends on the type of the expression. For example, in Java, floating point numbers use the IEEE 754 standard, and thus when an overflow occurs, the appropriate positive or negative infinity is returned. However, Java integers wrap on overflow. Consider the following examples.
(\product float f; 1.0e30f < f && f < 1.0e38f; f) == Float.POSITIVE_INFINITY (\sum int i; i == Integer.MAX_VALUE  i == 1; i) == Integer.MAX_VALUE + 1 == Integer.MIN_VALUEWhen the range predicate is not satisfiable, the sum is 0 and the product is 1; for example:
(\sum int i; false; i) == 0 (\product double d; false; d*d) == 1.0When the range predicate is not satisfiable for
\max
the result is the smallest number with the type of the expression in the body;
for floating point numbers, negative infinity is used.
Similarly, when the range predicate is not satisfiable for \min
,
the result is the largest number with the type of the expression in the body.
\num_of
, which is "numerical quantifier." It returns the number
of values for its variables for which the range and the expression in its
body are true. Both the range predicate and the body must have type boolean
, and the entire quantified expression has type long
.
The meaning of this quantifier is defined by the following equation
(see p. 57 of [Cohen90]).
(\num_of T x; R(x); P(x)) == (\sum T x; R(x) && P(x); 1L)
JMLObjectSet
that is the subset of nonnull Integer
objects
found in the set myIntSet
whose values are between 0 and 10, inclusive.
new JMLObjectSet {Integer i  myIntSet.has(i) && i != null && 0 <= i.getInteger() && i.getInteger() <= 10 }The syntax of JML (see the JML Reference Manual [LeavensetalJMLRef] for details) limits set comprehensions so that following the vertical bar (`

') is always an invocation of the has
method of some set on the variable declared.
(This restriction is used to avoid Russell's paradox
[WhiteheadRussell25].)
In practice, one either starts from some relevant set at hand,
or one can start from the sets containing the objects of primitive types
found in org.jmlspecs.models.JMLModelObjectSet
and (in the same Java package) JMLModelValueSet
.
The type of such an expression is the type named following
new
, which must be JMLObjectSet
or JMLValueSet
.
\duration
, which describes the specified maximum number of
virtual machine cycle times needed to execute the method call or
explicit constructor invocation expression that is its argument;
e.g., \duration(myStack.push(o))
is the maximum number of
virtual machine cycles needed to execute the call myStack.push(o)
,
according to the contract of the static type of myStack
's
type's push
method, when passed argument o
.
Note that the expression used as an argument to \duration
should be thought of as quoted, in the sense that it is not to be
executed; thus the method or constructor called need not be free
of side effects.
The argument expression must be a method call or explicit constructor
invocation expression;
the type of a \duration
expression is long
.
For a given Java Virtual Machine,
a virtual machine cycle is defined to be the minimum of
the maximum over all Java Virtual Machine instructions, i,
of the length of time needed to execute instruction i.
The keyword \duration
can only be used in the specexpression of a durationclause;
it cannot be used, for example, in postconditions.
\elemtype
, which returns the mostspecific static type
shared by all elements of its array argument [LeinoNelsonSaxe00].
For example, \elemtype(\type(int[]))
is \type(int)
.
The argument to \elemtype
must be an expression of type
\TYPE
, which JML considers to be the same as java.lang.Class
,
and its result also has type \TYPE
. If the argument is not an
array type, the result is null
.
\fresh
, which asserts that objects were freshly allocated;
for example, \fresh(x,y)
asserts that
x
and y
are not null
and that the objects bound to these identifiers
were not allocated in the prestate.
The arguments to \fresh
can have any reference type,
and the type of the overall expression is boolean
.(29)
\invariant_for
, which is true
just when its argument satisfies the invariant
of its static type; for example, \invariant_for((MyClass)o)
is true when o
satisfies the invariant of MyClass
.
The entire \invariant_for
expression is of type boolean
.
\is_initialized
, which is true
just when its referencetype argument is a class that has
finished its static initialization.
It is of type boolean
.
\lblneg
and \lblpos
can be used to attach labels to expressions [LeinoNelsonSaxe00];
these labels might be printed in various messages by support tools,
for example, to identify an assertion that failed.
Such an expression has a label and a body;
for example, in
(\lblneg indexInBounds 0 <= index && index < length)the label is
indexInBounds
and the body is the expression 0 <= index && index < length
.
The value of a labeled expression is the value of its body,
hence its type is the type of its body.
The idea is that if this expression is used in an assertion
and its value is false
(e.g., when doing runtime checking
of assertions), then a warning will be printed that includes
the label indexInBounds
.
The form using \lblpos
has a similar syntax,
but should be used for warnings when the value of the enclosed expression
is true
.
\lockset
, which is the set of locks held by the current thread.
It is of type JMLObjectSet
.
(This is an adaptation from ESC/Java [Leinoetal00]
[LeinoNelsonSaxe00] for dealing with threads.)
\nonnullelements
,
which can be used to assert that an array and its elements are all nonnull.
For example, \nonnullelements(myArray)
, is equivalent to
[LeinoNelsonSaxe00]
myArray != null && (\forall int i; 0 <= i && i < myArray.length; myArray[i] != null)
\not_modified
, which asserts that the values of objects
are the same in the poststate as in the prestate;
for example, \not_modified(xval,yval)
says that
xval
and yval
have the same value in the pre
and poststates (in the sense of an equals
method).
The keyword \not_modified
can only be used in an ensuresclause or a signalsclause;
it cannot be used, for example, in preconditions.
The type of a \not_modified
expression is boolean
.
\old
, which can be used to refer to values in the prestate;
e.g., \old(myPoint.x)
is the value of the x
field of the object myPoint
in the prestate.
The type of such an expression is the type of the expression it
contains;
for example the type of \old(myPoint.x)
is the type of myPoint.x
.
The keyword \old
can only be used in an ensuresclause, a signalsclause,
or a historyconstraint;
it cannot be used, for example, in preconditions.
\reach
expression
allows one to refer to the set of objects reachable from some particular object.
The syntax \reach(
x)
denotes the smallest JMLObjectSet
containing the object denoted by
x, if any,
and all objects accessible through all fields of objects in this set.
That is, if x is null
, then this set is empty
otherwise it contains x,
all objects accessible through all fields of x,
all objects accessible through all fields of these objects,
and so on, recursively.
If x denotes a model field (or data group), then
\reach(
x)
denotes the smallest JMLObjectSet
containing the objects
reachable from x or reachable from the objects referenced by
fields in that data group.
\result
, which, in an ensures
clause
is the value or object that is being returned by a method.
Its type is the return type of the method; hence it is a type error to
use \result
in a void method or in a constructor.
The keyword \result
can only be used in an ensuresclause;
it cannot be used, for example, in preconditions or in signals clauses.
\space
, which describes the amount of heap space, in bytes,
allocated to the object refered to by its argument;
e.g., \space(myStack)
is number of bytes in the heap
used by myStack
, not including the objects it contains.
The type of the specexpression that is the argument must be a
reference type, and the result type of a \space
expression is
long
.
The keyword \space
can only be used in the specexpression of a workingspaceclause;
it cannot be used, for example, in postconditions.
\typeof
, which returns the mostspecific dynamic type of an
expression's value [LeinoNelsonSaxe00].
The meaning of \typeof(
E)
is unspecified if E is null.
If E has a static type that is a reference type,
then \typeof(
E)
means the same thing as
E.getClass()
.
For example, if c
is a variable of static type
Collection
that holds an object of class HashSet
,
then \typeof(c)
is HashSet.class
, which is the same
thing as \type(HashSet)
.
If E has a static type that is not a reference type,
then \typeof(
E)
means the instance of java.lang.Class
that represents its static type.
For example, \typeof(true)
is Boolean.TYPE
, which is the
same as \type(boolean)
.
Thus an expression of the form \typeof(
E)
has
type \TYPE
, which JML considers to be the same as
java.lang.Class
.
<:
, which compares two reference types and returns true
when the type on the left is a subtype of the type on the right
[LeinoNelsonSaxe00].
Although the notation might suggest otherwise,
this operator is also reflexive;
a type will compare as <:
with itself.
In an expression of the form E1 <:
E2,
both E1 and E2 must have type \TYPE
;
since in JML \TYPE
is the same as java.lang.Class
the expression E1 <:
E2 means the same thing as the expression
E2.isAssignableFrom(
E1)
.
\type
, which can be used to mark types in expressions.
An expression of the form \type(T)
has the type \TYPE
.
Since in JML \TYPE
is the same as java.lang.Class
,
an expression of the form \type(
T)
means the same thing as T.class
.
For example, in
\typeof(myObj) <: \type(PlusAccount)the use of
\type(PlusAccount)
is used to introduce
the type PlusAccount
into this expression context.
\working_space
, which describes the maximum specified amount of
heap space, in bytes, used by the
method call or explicit constructor invocation expression that is its argument;
e.g., \working_space(myStack.push(o))
is the maximum number of
bytes needed on the heap to execute the call myStack.push(o)
,
according to the contract of the static type of myStack
's
type's push
method, when passed argument o
.
Note that the expression used as an argument to \working_space
should be thought of as quoted, in the sense that it is not to be
executed; thus the method or constructor called need not be free
of side effects.
The argument expression must be a method call or explicit constructor
invocation expression;
the result type of a \working_space
expression is long
.
The keyword \working_space
can only be used in the specexpression of a workingspaceclause;
it cannot be used, for example, in postconditions.
As in Java itself, most types are reference types, and hence many expressions
yield references (i.e., object identities or addresses),
as opposed to primitive values.
This means that ==
, except when used to compare
pure values of primitive types such as boolean
or int
,
is reference equality.
As in Java,
to get value equality for reference types one uses the
equals
method in assertions.
For example, the predicate
myString == yourString
, is only true if
the objects denoted by myString
and yourString
are the
same object (i.e., if the names are aliases);
to compare their values one must write
myString.equals(yourString)
.
The reference semantics makes interpreting predicates that involve
the use of \old
interesting.
We want to have the semantics suited for two purposes:
The key to the semantics of \old
is to treat it as an abbreviation for a local definition.
That is, E in \old(
E)
can be evaluated in the prestate, and its value bound to a
locally defined name,
and then the name can be used in the postcondition.
To avoid referring to the value of uninitialized locations, a constructor's precondition can only refer to locations in the object being constructed that are not assignable. This allows a constructor to refer to instance fields of the object being constructed if they are not made assignable by the constructor's assignable clause, for example, if they are declared with initializers. In particular, the precondition of a constructor may not mention a "blank final" instance variable that it must assign.
Since we are using Java expressions for predicates, there are some additional problems in mathematical modeling. We are excluding the possibility of sideeffects by limiting the syntax of predicates, and by using type checking [GiffordLucassen86] [Lucassen87] [LucassenGifford88] [NielsonNielsonAmtoft97] [TalpinJouvelot94] [Wright92] to make sure that only pure methods and constructors may be called in predicates.
Exceptions in expressions are particularly important,
since they may arise in type casts.
JML deals with exceptions
by having the evaluation
of predicates substitute an arbitrary expressible value of the
normal result type when an exception is thrown during evaluation.
When the expression's result type is a reference type,
an implementation would have to return null
if an exception is thrown while executing such a predicate.
This corresponds to a mathematical model in which partial functions
are mathematically modeled by underspecified total functions
[GriesSchneider95].
However, tools sometimes only approximate this semantics.
In tools, instead of fully catching exceptions for all subexpressions,
many tools only catch exceptions for the smallest booleanvalued subexpression
that may throw an exception (and for entire expressions used
in JML's measuredclause and variantfunction).
JML will check that errors (i.e., exceptions that inherit from Error) are not explicitly thrown by pure methods. This means that they can be ignored during mathematical modeling. When executing predicates, errors will cause runtime errors.
The grammatical production storeref
(see the JML Reference Manual [LeavensetalJMLRef] for the exact syntax)
is used to name locations
in the assignable
, in
, mapsinto
, and
represents
clauses. A similar production for objectref
is used in the accessible
clause.
A storeref names a location, not an object;
a location is either a field of an object, or an array element.
Besides the Java syntax of names and field and array references,
JML supports the following syntax for storerefs.
See the JML Reference Manual [LeavensetalJMLRef] for more
details on the syntax.
[
E1 ..
E2]
,
denote the locations in the array A between the value of E1
and the value of E2 (inclusive).
For example, the clause
assignable myArray[3 .. 5]can be thought of an abbreviation for the following.
assignable myArray[3], myArray[4], myArray[5]
[*]
, which is shorthand for
A[0 ..
A.length1]
.
.*
names all of the nonstatic fields of the object referred to by x.
For example, if p
is a Point
object with two fields,
x
and y
of type BigInteger
,
then p.*
names the fields p.x
and p.y
.
Notice that the fields of the BigInteger
objects are not named.
Also, p.*.*
is not allowed.
a
is an array of type Rocket []
,
then the storeref a[*].*
means all of the
nonstatic fields of each Rocket
object referred to by the elements of array a
.
Go to the first, previous, next, last section, table of contents.